Towards a Verified CPS translation for CertiCoq

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.