Formal verification of closure conversion
CertiCoq is a formally verified compiler for dependently typed functional languages that aims to bridge the gap between certified high-level programs and their translation to a low-level machine language. In this talk I will describe the process of implementing and proving correct, using machine checked proofs, the closure conversion phase of CertiCoq. The main transformation is preceded by a lambda lifting phase, that can be seen as an unboxing optimization for closure environments, and followed by a hoisting transformation, which flattens the structure of function definitions. As opposed to previous closure conversion implementations, our implementation decouples the lambda lifting phase from the closure conversion phase, allowing us to achieve a more modular design which is more amenable to formal verification. I will explain the implementation of the three phases as well as the proof techniques that were used to prove their correctness. Finally, I will focus on the challenges involved in the composition of the correctness proofs of the three phases.