CertiCoq 0.9 beta
Pre-release
Pre-release
We are happy to announce the release of CertiCoq 0.9beta. 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.
The CertiCoq Team