An Verified Optimizing Backend for a Purely Functional Language

---------------------------------------------------------------------------------------------------------

CertiCoq is a verified compiler for the source language of the interactive

theorem prover Coq. The goal of CertiCoq is to bridge the gap between a

certified source program and the compiled executable program. Coq's source

language, Gallina, is a pure functional language without side effects. To allow

programs to interact with their environment despite the lack of side effects,

CertiCoq compiles Gallina to C, where the program can be linked with C code that

handles the input and the output.

In my thesis, I focus on the design, the implementation, and the verification of

the optimizing backend of CertiCoq, that is responsible to efficiently compile

untyped higher-order functional code to a first-order representation ready to be

complied to C. The design of the CertiCoq backend follows a micropass compiler

architecture that consists of small compiler passes each of them performing a

simple task, and optimizations in the final code rely on the interaction of

these transformations. To prove the set of backend transformations correct, I

developed a proof framework based on step-indexed logical relations, a powerful

proof technique that is used to show program equivalence. The modular and

compositional nature of logical relations greatly fits the architecture of our

compiler, allowing for proof reuse and compositional reasoning. Despite their

mathematical elegance, logical relations cannot generally be used to show

correctness of separate compilation in multi-pass compilers. I show how our

existing proof framework can be extended to provide guarantees not only about

whole-program compilation, but also about the correctness of the interaction of

programs that are compiled separately through CertiCoq, perhaps using different

backend optimizations. This is the first time that logical relations are used to

obtain a proof of correctness for separate compilation.

In the second part of my thesis, I show how to strengthen the guarantees that

the proof framework provides, but from a different angle. Bugs in compilers

manifest themselves not only in the final result of the computation, what we

usually call functional correctness of the transformation, but also in other

observable behaviours of the program, such as resource consumption. In order to

ensure that a transformation will not introduce timing and memory leaks, I

extended the logical relation framework so that it supports reasoning about

preservation of running time and space. I used this extended proof framework to

prove that the closure conversion algorithm of CertiCoq is not only correct with

respect to the final result, but also safe for space. Furthermore, I also show

that the garbage collection strategy followed by CertiCoq is safe with respect

to the idealistic space consumption model. This is the first formal proof of

space-safety for a closure conversion algorithm and a particular garbage

collection strategy and also the first time that logical relations were used to

reason about space safety.