An Inductive Proof Method for Simulation-based Compiler Correctness

This is the Coq development accompanying our recent submission to CPP. Coq sources are available for download.

In previous work we introduced the intermediate language IL, a first-order language with system calls. IL has two semantics, which interpret variables differently, as binders or as assignables. In this work we present an inductive proof method for simulation-based compiler correctness. We showcase the method with the proof of dead code elimination (DCE), which consists of the following two optimizations:

1. Unreachable Code Elimination
2. Dead Variable Elimination

The correctness proofs of UCE and DVE require an interesting simulation argument: In both cases a step must be argued where the source program reduces (for example, a variable definition) whereas the target program does not reduce (because the variable definition has been removed). Our proof method is induction on the program structure, facilitated by a fixed-point lemma about our simulation, which we call the extension lemma. We prove the extension lemma for the imperative interpretation and for the functional interpretation.

We specify soundness of unreachable code, implement unreachable code elimination (UCE) and prove it correct. We show correctness for both semantic interpretations of IL.

We specify soundness of liveness, implement dead variable elimination (DVE) and prove it correct. Again, we show correctness for both semantic interpretations of IL.

Selected Items from the Table of Contents