We are happy to announce the release of CertiCoq 0.9 for Coq 8.19. CertiCoq is a formally verified compiler from Gallina, the internal language of Coq down to CompCert Clight. It can be used to compile Coq programs to C programs which can be further compiled with compcert or any other C compiler. See the CertiCoq wiki for a detailed description of the project and provided plugins. This release adds support for the compilation of primitive integers and floating point types and benefits from the optimization phases from MetaCoq 1.3.1.
The CertiCoq Team