CertiCoq</img    

Principled Optimizing Compilation of Dependently Typed Programs

The CertiCoq project aims to build a proven-correct compiler for dependently-typed, functional languages, such as Gallina—the core language of the Coq proof assistant. A proved-correct compiler consists of a high-level functional specification, machine-verified 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 dependently-typed languages.

Andrew Appel
Andrew W. Appel

Princeton University
Greg Morrisett
Greg Morrisett

Cornell University
Randy Pollack
Randy Pollack

Edinburgh University
Matthieu Sozeau
Matthieu Sozeau

INRIA Paris
Olivier Savary Belanger
Olivier Savary Belanger

Princeton University
Zoe Paraskevopoulou
Zoe Paraskevopoulou

Princeton University
Abhishek Anand
Abhishek Anand

Cornell University
Matthew Weaver
Matthew Weaver

Princeton University
   DeepSpec

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.

Trust.
Current compilers for these languages are not proved correct; they must be trusted. These compilers do not even use typed intermediate languages, as foundational problems arise when attempting classical compiler transformations, such as CPS- and closure-conversion.
Performance.
Compilers for these languages produce code that performs poorly when compared to conventional languages. This is due in part to the lack of a proper phase distinction between terms needed only for type-checking, and those needed for execution. Also, current compilers fail to take advantage of the structure in these languages. For example, they either use a fully-eager or fully-lazy strategy, when a mixed strategy might be better.
Side-effects
are not supported in these languages for reasons of logical consistency. Though some previous work, including our own, suggests how to lift this constraint, the proof obligations from these approaches make programming very hard.

We will address these issues by exploring the design and implementation of a high-performance, 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 CCF-1407790 and CCF-1407794, 2014-2017.