Calculating correct compilers

Article English OPEN
Bahr, Patrick ; Hutton, Graham (2015)

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.
  • References (27)
    27 references, page 1 of 3

    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.

  • Metrics
    No metrics available
Share - Bookmark