CertiCoq

Overview

CertiCoq is a compiler for Gallina, the specification language of the Coq proof assistant. CertiCoq targets Clight, a subset of the C language that can be compiled with any C compiler, including the CompCert verified compiler.

The goal of the CertiCoq project is to build an end-to-end verified compiler for Gallina, bridging the gap between formally verified source programs and their compiled executables.

Large parts of the CertiCoq compiler have been verified whereas others are in the process of being verified.

You can find CertiCoq’s souce code on GitHub.

Current Members

Andrew Appel, Yannick Forster, Anvay Grover, Joomy Korkut, John Li, Zoe Paraskevopoulou, and Matthieu Sozeau.

Past Members and Contributors

Abhishek Anand, Greg Morrisett, Randy Pollack, Olivier Savary Belanger, Matthew Weaver

Documentation

The CertiCoq Wiki has instructions for using the CertiCoq plugin to compile Gallina to C and interfacing with the generated C code.

The Wiki also gives an overview of the compiler and its verification status.

Publications

• Closure Conversion is Safe for Space, Zoe Paraskevopoulou and Andrew W. Appel. Proceedings of the ACM on Programming Languages, vol. 3, no. ICFP, article 83, 29 pages, doi 10.1145/3341687, August 2019.

• Shrink Fast Correctly! Olivier Savary Belanger and Andrew W. Appel. Proceedings of International Symposium on Principles and Practice of Declarative Programming (PPDP’17), pages 49-60, ACM Press, October 2017 (PPDP’17).

• CertiCoq: A verified compiler for Coq. 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.

License

CertiCoq is open source and distributed under the MIT license.

Bugs

We use github’s issue tracker to keep track of bugs and feature requests.