Home

Welcome to the CertiCoq wiki. The Wiki provides documentation for the CertiCoq compiler.

Contents

1. The CertiCoq Plugin
   Useful information about the usage of the CertiCoq plugin.
2. The bootstrapped CertiCoqC and CertiCoqChk Plugins
   Useful information about the bootstrapped plugins.
3. The CertiCoq Pipeline
   Information about the CertiCoq pipeline and its current verification status.
4. Glue Code and FFI
   Information about interfacing with the generated C code.
5. Memory Model and Garbage Collection
   Lightweight description of CertiCoq's memory representation and runtime.
6. When C code allocates on the Coq heap
   How to write C functions that interface with Coq functions