Skip to content

CertiCoq/certicoq

Folders and files

NameName
Last commit message
Last commit date

Latest commit

59be195 · Jan 27, 2025
Aug 21, 2024
Aug 20, 2024
Aug 20, 2024
Aug 20, 2024
Aug 20, 2024
Jan 27, 2025
Oct 10, 2022
Aug 20, 2024
Aug 20, 2024
Aug 20, 2024
Jan 27, 2025
Mar 26, 2024
Feb 11, 2022
Feb 11, 2022
Dec 21, 2020
Aug 20, 2024
Dec 31, 2024
Oct 10, 2022
Sep 30, 2022
Oct 14, 2022
Jan 27, 2025
Jul 21, 2022
Jan 29, 2022

Repository files navigation

CertiCoq

CertiCoqCoq

Overview

build

GitHub

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.

Documentation

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.

Installation Instructions

See INSTALL.md for installation instructions.

Current Members

Andrew Appel, Yannick Forster, Joomy Korkut, Zoe Paraskevopoulou, and Matthieu Sozeau.

Past Members and Contributors

Abhishek Anand, Anvay Grover, John Li, Greg Morrisett, Randy Pollack, Olivier Savary Belanger, Matthew Weaver

License

CertiCoq is open source and distributed under the MIT license.

Directory structure

  • theories/ contains the sources of the compiler
  • plugin/ contains the CertiCoq plugin for Coq
  • benchmarks/ contains the benchmark suite
  • glue/ contains the glue code generator
  • bootstrap/ 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 utilities
  • theories/Compiler: contains the toplevel CertiCoq pipeline
  • theories/LambdaBoxMut: mutual inductive version of MetaCoq's LambdaBox erased language
  • theories/LambdaBoxLocal: variant where deBruijn indices are represented using N instead of nat. The transformation from LambdaBoxMut let-binds the definitions in the environment to produce a closed term.
  • theories/LambdaANF contains the λANF pipeline (and conversions -- direct and LambdaANF -- to λANF)
  • theories/Codegen contains the C code generator.

Bugs

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