An Inductive Proof Method for Simulation-based Compiler Correctness

TL;DR

This paper introduces an inductive proof method for bisimulation-based compiler correctness, effectively handling dead code elimination and related transformations within a formal Coq framework.

Contribution

It generalizes compatibility of function definitions for inductive proofs, enabling natural reasoning about complex program transformations like dead code elimination.

Findings

Successfully formalized in Coq

Proved correctness of dead code elimination

Handles recursive functions and system calls

Abstract

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.