Patrick Bahr IT University of Copenhagen

Calculating Correct Compilers

Patrick Bahr, presenting joint work with Graham Hutton
Talk, FP Lunch, Functional Programming Lab, University of Nottingham, UK, 11/10/2013.


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