Publication details

Saarland University Computer Science

An Inductive Proof Method for Simulation-based Compiler Correctness

Sigurd Schneider, Gert Smolka, Sebastian Hack

Technical Report, Saarland University, November 2016

We study induction on the program structure as a proof method for bisimulation-based compiler correctness. We consider a first-order language with mutually recursive function definitions, system calls, and an environment semantics. The proof method relies on a generalization of compatibility of function definition with the bisimulation. We use the inductive method to show correctness of a form of dead code elimination. This is an interesting case study because the transformation removes function, variable, and parameter definitions from the program. While such transformations require modification of the simulation in a coinductive proof, the inductive method deals with them naturally. All our results are formalized in Coq.

Link to Paper on ArXiv Link to Coq Formalization

Show BibTeX               

Login to edit

Legal notice, Privacy policy