Olivier Savary Belanger will present his Pre FPO on Thursday, March 7, 2019 at 10am in CS 402. The members of his committee are as follows: Andrew Appel (adviser), Greg Morrisett (Cornell), David Walker, Zak Kincaid, and Lennart Beringer All are welcome to attend. Please see below for the talk abstract. Interactive theorem provers allow for the development, in the same environment, of programs and of proofs about them. The programmatic portion of the development can then be extracted to code which is then compiled in an executable. However, unless both the extraction and compilation processes are formally verified, one has no guarantees that the proofs developed still apply to the resulting executable. In this talk, I will describe my work on CertiCoq, a verified extraction pipeline for the Coq theorem prover composing with the CompCert C verified compiler to achieve end-to-end correctness guarantees. First, I will present a proof framework to prove optimizations over the continuation-passing style (CPS) intermediate representation (IR) used in CertiCoq. This framework has been used by myself and others to prove the correctness of nontrivial optimizations. I will focus on a novel proof of correctness for a shrink reduction algorithm, a transformation combining in a single pass multiple optimizations which always result in smaller terms. Then, I will present a verified code generation translating the CPS IR into Clight, a front-end language of CompCert. I will show how it interfaces with a verified garbage collector and how its proof composes with the proof of correctness on CompCert. I will also describe the representation of values of inductive datatypes, inspired by OCaml, and the generated interface between the extracted program and regular C code.