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.