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 CertiCoq Pipeline
   Information about the CertiCoq pipeline and its current verification status.
3. Glue Code and FFI
   Information about interfacing with the generated C code.
4. Memory Model and Garbage Collection
   Lightweight description of CertiCoq's memory representation and runtime.