Patrick Bahr Associate Professor, IT University of Copenhagen

Calculating Correct Compilers

Patrick Bahr, presenting joint work with Graham Hutton
Talk, 22nd Dutch Functional Programming Day 2014, University of Amsterdam, The Netherlands, 10/01/2014.


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