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.
Large parts of the CertiCoq compiler have been verified whereas others are in the process of being verified.
The CertiCoq Wiki has instructions for using the CertiCoq plugin to compile Gallina to C and interfacing with the generated C code.
You can also find some demos here and here.
See INSTALL.md for installation instructions.
Andrew Appel, Yannick Forster, Anvay Grover, Joomy Korkut, John Li, Zoe Paraskevopoulou, and Matthieu Sozeau.
Abhishek Anand, Greg Morrisett, Randy Pollack, Olivier Savary Belanger, Matthew Weaver
CertiCoq is open source and distributed under the MIT license.
theories/contains the sources of the compilerplugin/contains the CertiCoq plugin for Coqbenchmarks/contains the benchmark suiteglue/contains the glue code generatorbootstrap/contains the bootstrapped CertiCoq plugin for Coq and a CertiCoq-compiled variant of MetaCoq's safe type checker.
Structure of the theories directory:
theories/common: contains common code utilitiestheories/Compiler: contains the toplevel CertiCoq pipelinetheories/LambdaBoxMut: mutual inductive version of MetaCoq's LambdaBox erased languagetheories/LambdaBoxLocal: variant where deBruijn indices are represented usingNinstead ofnat. The transformation from LambdaBoxMut let-binds the definitions in the environment to produce a closed term.theories/LambdaANFcontains the λANF pipeline (and conversions -- direct and LambdaANF -- to λANF)theories/Codegencontains the C code generator.
We use github's issue tracker to keep track of bugs and feature requests.