Remember Me
Or use your Academic/Social account:


Or use your Academic/Social account:


You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.


Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message


Verify Password:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Bahr, Patrick; Hutton, Graham (2015)
Publisher: Cambridge University Press
Languages: English
Types: Article

Classified by OpenAIRE into

arxiv: Computer Science::Programming Languages
In this article we present a new approach to the problem of calculating compilers. In particular, we develop a simple but general technique that allows us to derive correct compilers from high- level semantics by systematic calculation, with all details of the implementation of the compilers falling naturally out of the calculation process. Our approach is based upon the use of standard equational reasoning techniques, and has been applied to calculate compilers for a wide range of language features and their combination, including arithmetic expressions, exceptions, state, various forms of lambda calculi, bounded and unbounded loops, non-determinism, and interrupts. All the calculations in the article have been formalised using the Coq proof assistant, which serves as a convenient interactive tool for developing and verifying the calculations.
  • The results below are discovered through our pilot algorithms. Let us know how we are doing!

    • Adams, Norman, Kranz, David, Kelsey, Richard, Rees, Jonathan, Hudak, Paul, & Philbin, James. (1986). ORBIT: An Optimizing Compiler for Scheme. Pages 219-233 of: Proceedings of the 1986 SIGPLAN Symposium on Compiler Construction. ACM.
    • Ager, Mads Sig, Biernacki, Dariusz, Danvy, Olivier, & Midtgaard, Jan. (2003a). A Functional Correspondence Between Evaluators and Abstract Machines. Pages 8-19 of: Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming. ACM.
    • Ager, Mads Sig, Biernacki, Dariusz, Danvy, Olivier, & Midtgaard, Jan. (2003b). From Interpreter to Compiler and Virtual Machine: A Functional Derivation. Technical Report RS-03-14. BRICS, Department of Computer Science, University of Aarhus.
    • Appel, Andrew. (1991). Compiling with Continuations. Cambridge University Press.
    • Backhouse, Roland. (2003). Program Construction: Calculating Implementations from Specifications. John Wiley and Sons, Inc.
    • Bahr, Patrick. (2014). Proving Correctness of Compilers Using Structured Graphs. Pages 221-237 of: Functional and Logic Programming. Lecture Notes in Computer Science, vol. 8475. Springer International Publishing.
    • Chase, David. (1994a). Implementation of Exception Handling, Part I. The Journal of C Language Translation, 5(4), 229-240.
    • Chase, David. (1994b). Implementation of Exception Handling, Part II. The Journal of C Language Translation, 6(1), 20-32.
    • Day, Laurence E., & Hutton, Graham. (2014). Compilation a` la Carte. Pages 13-24 of: Proceedings of the 25th Symposium on Implementation and Application of Functional Languages. ACM.
    • Dybjer, Peter. (1994). Inductive Families. Formal Aspects of Computing, 6(4), 440-465.
    • Hutton, Graham. (2007). Programming in Haskell. Cambridge University Press.
    • Hutton, Graham, & Wright, Joel. (2004). Compiling Exceptions Correctly. Pages 211- 227 of: Mathematics of Program Construction. Lecture Notes in Computer Science, vol. 3125. Springer Berlin / Heidelberg.
    • Hutton, Graham, & Wright, Joel. (2007). What is the Meaning of These Constant Interruptions? Journal of Functional Programming, 17(06), 777-792.
    • Letouzey, Pierre. (2008). Extraction in Coq: An Overview. Pages 359-369 of: Logic and Theory of Algorithms: 4th Conference on Computability in Europe. Lecture Notes in Computer Science, vol. 5028. Springer-Verlag.
    • McCarthy, John, & Painter, James. (1967). Correctness of a Compiler for Arithmetic Expressions. Pages 33-41 of: Mathematical Aspects of Computer Science. Proceedings of Symposia in Applied Mathematics, vol. 19. American Mathematical Society.
    • McKinna, James, & Wright, Joel. (2006). A Type-Correct, Stack-Safe, Provably Correct Expression Compiler in Epigram. Unpublished manuscript.
    • Meijer, Erik. (1992). Calculating Compilers. Ph.D. thesis, Katholieke Universiteit Nijmegen.
    • Reynolds, John C. (1972). Definitional Interpreters for Higher-Order Programming Languages. Pages 717-740 of: Proceedings of the ACM Annual Conference. ACM.
    • Sculthorpe, Neil, Farmer, Andrew, & Gill, Andy. (2013). The HERMIT in the Tree: Mechanizing Program Transformations in the GHC Core Language. Pages 86-103 of: Implementation and Application of Functional Languages 2012. Lecture Notes in Computer Science, vol. 8241. Springer.
    • Sestoft, Peter. (1997). Deriving a Lazy Abstract Machine. Journal of Functional Programming, 7(03), 231-264.
    • Spivey, Mike. (1990). A Functional Theory of Exceptions. Science of Computer Programming, 14(1), 25-42.
    • Steele, Jr., Guy L. (1978). Rabbit: A Compiler for Scheme. Tech. rept. AI-TR-474. MIT AI Lab.
    • Thielecke, Hayo. (2002). Comparing Control Constructs by Double-Barrelled CPS. Higher-Order and Symbolic Computation, 15(2-3), 141-160.
    • Wadler, Philip. (1989). Theorems for Free! Pages 347-359 of: Proceedings of the fourth International Conference on Functional Programming Languages and Computer Architecture. ACM Press.
    • Wand, Mitchell. (1982a). Deriving Target Code as a Representation of Continuation Semantics. ACM Trans. on Programming Languages and Systems, 4(3), 496-517.
    • Wand, Mitchell. (1982b). Semantics-Directed Machine Architecture. Pages 234-241 of: Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM.
    • Winskel, Glynn. (1993). The Formal Semantics of Programming Languages - An Introduction. Foundation of Computing Series. MIT Press.
  • No related research data.
  • No similar publications.

Share - Bookmark

Cite this article