Proving Correctness of Compilers Using Structured Graphs

Coq proofs for the paper "Proving Correctness of Compilers Using Structured Graphs".

File Structure

• Tree.v, Graph.v: Definition of tree and graph types, respectively.
• GraphUnravel.v: Proof of Theorem 2.
• Compiler.v: Implementation of the tree-based and the graph-based compiler; proof of Lemma 1 from the paper.
• CalculationTactics.v: Tactics for program calculation proofs.
• Container.v: Formalisation of containers (used as a representation of strictly positive functors).

Technical Details

Dependencies

• To check the proofs: Coq 8.4pl5
• To step through the proofs: GNU Emacs 24.3.1, Proof General 4.2

Proof Checking

To check and compile the complete Coq development, you can use the Makefile:

> make