Skip to content

Releases: CertiCoq/certicoq

CertiCoq 0.9 for Coq 8.19

28 May 12:45
@mattam82 mattam82
v0.9+8.19
5685b3d
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Learn about vigilant mode.
Compare
Choose a tag to compare
CertiCoq 0.9 for Coq 8.19 Latest
Latest

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

Assets 3
Loading

CertiCoq 0.9 beta

11 Oct 22:58
@mattam82 mattam82
v0.9-beta
87dff37
Compare
Choose a tag to compare
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

Assets 2
Loading