This repository contains the supplementary material for the paper Calculating Correct Compilers II: Return of the Register Machines by Patrick Bahr and Graham Hutton. The material includes Coq formalisations of all calculations in the paper along with the full Haskell source code of the calculated compilers. In addition, we also include Coq formalisations for calculations that were mentioned but not explicitly carried out in the paper.
The Coq formalisation is located in the coq subfolder. Below we list the Coq files for the calculations from the paper and the specification of the memory model:
- Memory.v: the (axiomatic) memory model (Section 2)
- Arith.v: arithmetic expressions (section 3)
- Exception.v: arithmetic expressions + exceptions (section 4)
- Lambda.v: call-by-value lambda calculus (section 5)
We also include compiler calculations for additional languages:
- State.v: global state + exceptions
- LocalState.v: local state + exceptions
- LambdaBad.v: call-by-value lambda calculus without a stack which yields an unsatisfactory compiler and machine
- LambdaTruncate.v: variant of Lambda.v is more realistic as it only copies a bounded set of registers to the stack (via truncation)
- LambdaException.v: lambda calculus + exceptions, based on LambdaTruncate.v
- While.v: state + while loops
- WhileCoalesced.v: Variant of While.v with a semantics better suited for calculation
- ExceptionPartial.v: variant of Exception.v with an expclicit empty exception handler (for unhandled exceptions)
- ExceptionTwo.v: variant of Exception.v that compiles exceptions away by using two code continuations
The remaining files are used to define the Coq tactics to support reasoning in calculation style and to provide auxiliary concepts:
- Tactics.v: tactics for calculation style proofs
- Machine.v: auxiliary definitions and tactics for virtual machines
- LinearMemory.v: instantiation of the memory model (thus proving its consistency)
- ListIndex.v: definitions to index elements in a list
The haskell subfolder contains the source code of the three compilers calculated in the paper:
- arith.lhs: arithmetic expressions (section 3)
- except.lhs: arithmetic expressions + exceptions (section 4)
- lambda.lhs: lambda calculus (section 5)