Skip navigation
Please use this identifier to cite or link to this item:
Title: Towards a Verified CPS translation for CertiCoq
Authors: Grover, Anvay
Advisors: Appel, Andrew
Department: Computer Science
Class Year: 2020
Abstract: CertiCoq is a verified-in-Coq compiler from Coq’s Gallina language throughCompCertC to assembly language, written as a Coq program. Here we describe the implementation and Coq verification of one of CertiCoq’s compiler passes which translates a deBruijn-based intermediate language to a continuation passing style (CPS) intermediate language. This translation is critical because the CPS intermediate language precedes the optimization passes of CertiCoq. We improve upon the existing CertiCoq compiler pipeline, which is circuitous and does several intermediate transformations before reaching the CPS language. Our Coq verification makes progress towards showing that the semantics of the source language are preserved in any programs in the CPS language. We provide the algorithm used for our CPS translation, define an environment-based semantics for the deBruijn-based intermediate language which we then prove equivalent to the substitution semantics, and describe progress towards the semantics preservation proof of the CPS transformation.
Type of Material: Princeton University Senior Theses
Language: en
Appears in Collections:Computer Science, 1988-2020

Files in This Item:
File Description SizeFormat 
GROVER-ANVAY-THESIS.pdf256.4 kBAdobe PDF    Request a copy

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