Please use this identifier to cite or link to this item: http://arks.princeton.edu/ark:/88435/dsp015m60qv74k
 Title: Specification of the Dead Parameter Elimination Optimization of the CertiCoq Compiler Authors: Vassilev, Katja Advisors: Dvir, ZeevAppel, Andrew Department: Mathematics Class Year: 2019 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. URI: http://arks.princeton.edu/ark:/88435/dsp015m60qv74k Type of Material: Princeton University Senior Theses Language: en Appears in Collections: Mathematics, 1934-2020