Zoe Paraskevopoulou will present her FPO "Verified Optimizations for Functional Languages" on Friday, 10/30/2020 at 3pm via Zoom. Zoom link: [ https://princeton.zoom.us/j/5655804837 | https://princeton.zoom.us/j/5655804837 ] The members of her committee are as follows: Andrew Appel (Adviser); Readers: Davis Walker and Amal Ahmed (Northeastern University); Examiners: Zachary Kincaid, Aarti Gupta, Davis Walker, Andrew Appel, Amal Ahmed (Northeastern University) A copy of her thesis is available upon request. Please email ngotsis@cs.princeton if you would like a copy of the thesis. Everyone is invited to attend her talk. Abstract follows below: Coq is one of the most widely adopted proof development systems. It allows programmers to write purely functional programs and verify them against specifications with machine-checked proofs. After verification, one can use Coq’s extraction plugin to obtain a certified program (in OCaml, Haskell, or Scheme) that can be compiled and executed. However, bugs in either the extraction function or the compiler of the extraction language, can render source level verification useless. A verified compiler is a compiler whose output provably preserves the semantics of the source language. CertiCoq is a currently developed verified compiler for Gallina, Coq’s specification language. With CertiCoq, one could obtain an executable program that has is guaranteed to have the same behavior as the source program, bridging the gap between the formally verified source program and the executable. In this thesis, I present the implementation and verification of CertiCoq’s optimizing middle-end pipeline. CertiCoq’s middle end consists of seven di↵erent transformations and is responsible for eciently compiling an untyped purely functional intermediate language to a first-order subset of this language, which can be readily compiled to a first-order, low-level intermediate language. CertiCoq’s middle-end pipeline performs crucial optimizations for functional languages including closure conversion, uncurrying, shrink-reduction and inlining. It advances the state of the art of verified optimizing compilers for functional languages by implementing ecient closure-allocation strategies. For proving CertiCoq correct, I develop a framework based on the technique of logical relations, making novel technical contributions. I extend the logical relation with notions of precondition and postcondition showing how it can be used to reason about intensional properties of programs simultaneously with extensional properties. I demonstrate how this allows reasoning about divergence preservation, which is not supported by traditional logical relations. I develop a novel, lightweight technique that allows logical-relation proofs to be composed, enabling verified separate compilation of programs compiled with CertiCoq using di↵erent sets of optimizations. Lastly, I use the framework to prove that CertiCoq’s closure conversion is not only functionally correct but also safe for time and space, meaning that it is guaranteed to preserve the asymptotic time and space complexity of the source program.