Skip navigation
Please use this identifier to cite or link to this item:
Title: Specification of the Dead Parameter Elimination Optimization of the CertiCoq Compiler
Authors: Vassilev, Katja
Advisors: Dvir, Zeev
Appel, 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.
Type of Material: Princeton University Senior Theses
Language: en
Appears in Collections:Mathematics, 1934-2020

Files in This Item:
File Description SizeFormat 
VASSILEV-KATJA-THESIS.pdf631.07 kBAdobe PDF    Request a copy

Items in Dataspace are protected by copyright, with all rights reserved, unless otherwise indicated.