Calculating Correct Compilers

Abstract

We present a new approach to the longstanding problem of calculating compilers. In particular, we develop a simple but general recipe that allows us to derive correct compilers from high-level semantics by systematic calculation, with all the required compilation machinery falling naturally out of the calculation process. Our approach is based upon a new application of well-known transformation techniques, and has been applied to calculate compilers for a wide range of language features and their combination, including arithmetic, exceptions, local and global state, various forms of lambda calculi, bounded and unbounded loops, non-determinism, and interrupts.

Categories: Compilers, Formal Verification

Tags: Compiler, Virtual Machine, Calculation, Constructive Induction, Defunctionalisation, Contiuation-passing Style, Semantics, Lambda Calculus