Specification of the Dead Parameter Elimination Optimization of the CertiCoq Compiler

Abstract

Dead parameter elimination is an optimization which can be performed on programs in an intermediate phase of the CertiCoq compiler to eliminate parameters which are not live in the function. Here, I provide an implementation of dead parameter elimination as well as an abstract relation $\leadsto_{live}$ which describes the transformation. I prove this relation correct with respect to the semantics of the CPS lambda calculus of the intermediate phase of the compiler. I also make use of existing relations on such programs in the proofs presented. We also show that the transformation preserves the time and space of the input program. The proofs are written and verified in Coq.