Principled Optimizing Compilation of Dependently Typed ProgramsThe CertiCoq project aims to build a provencorrect compiler for dependentlytyped, functional languages, such as Gallinaâ€”the core language of the Coq proof assistant. A provedcorrect compiler consists of a highlevel functional specification, machineverified proofs of important properties, such as safety and correctness, and a mechanism to transport those proofs to the generated machine code. The project exposes both engineering challenges and foundational questions about compilers for dependentlytyped languages. 
Andrew W. Appel Princeton University 
Greg Morrisett Cornell University 
Randy Pollack Edinburgh University 
Matthieu Sozeau INRIA Paris 

Olivier Savary Belanger Princeton University 
Zoe Paraskevopoulou Princeton University 
Abhishek Anand Cornell University 
Matthew Weaver Princeton University 
The rise of dependently typed languages has enabled the construction of certified programs which come equipped with proofs of correctness. In particular, Coq has been used to build certified compilers, web servers and clients, databases, and decision procedures. While these developments are exciting, there are a number of problems that prevent us from using dependently typed languages for realistic systems.
We will address these issues by exploring the design and implementation of a highperformance, extensible, and certified compiler for Coq. Our compiler will use a mix of advanced, dependently typed intermediate languages and certified compilation to realize a trustworthy target. We will explore language extensions, analyses, and transformations to support efficient treatment of effects, mixed evaluation strategies, and a proper phase distinction.
CertiCoq: A verified compiler for Coq, by Abhishek Anand, Andrew Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu Sozeau, and Matthew Weaver. In CoqPL'17: The Third International Workshop on Coq for Programming Languages, January 2017.
Supported by the National Science Foundation, grants CCF1407790 and CCF1407794, 20142017.