Zoe Paraskevopoulou will present her pre-FPO "An Verified Optimizing Backend for a Purely Functional Language" on January 14, 2020 in CS 402 at 10am. The members of her committee are: Andrew Appel (adviser), David Walker (reader), Amal Ahmed (Northeastern University), Aarti Gupta (non-reader), Zachary Kincaid (non-reader) Everyone is invited to attend her talk. The talk title and abstract follow below. 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.