Calculating Correct Compilers
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 compilers from semantics by a process of systematic calculation, with all the required compilation machinery falling naturally out of the calculation process itself. 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