certicoq
C compiler
A compiler for a subset of the C language that can be compiled with any standard C compiler, used in formal verification and proof assistance.
A Verified Compiler for Gallina, Written in Gallina
137 stars
15 watching
26 forks
Language: Coq
last commit: 5 months ago
Linked from 2 awesome lists
compilercoqformal-verificationgallina
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
| certicoq/veriffi | Enables verified interaction between Coq programs and C libraries | 39 |
 absint/compcert | A formally verified compiler for a subset of C that generates code for multiple architectures. | 1,901 |
 pa-ba/calc-comp | Formalizations of compiler design and virtual machine calculations in Coq | 30 |
 sigurdschneider/lvc | A compiler project that aims to formalize and verify the semantics of an intermediate language using Coq | 57 |
 c2lang/c2compiler | A C compiler written in the C2 language itself. | 703 |
 coq-community/coq-program-verification-template | A template project for verifying the correctness of C programs in Coq | 29 |
 querycert/qcert | A framework for developing and verifying domain-specific languages with a focus on compiler correctness and verification. | 56 |
 certigraph/certigraph | A verification toolset for graph-manipulating programs written in Coq. | 17 |
 l1mey112/crepl | A compiler and interpreter for executing C code on the fly as it is typed. | 29 |
 inria/velus | A formally verified compiler for the Lustre programming language | 63 |
 circify/circ | A compiler infrastructure for translating high-level languages into circuit forms used in cryptography and formal verification. | 289 |
 certikos/coqrel | A Coq-based library for establishing logical relations in formal verification and proof assistance | 20 |
 rui314/9cc | A compiler project that compiles C code to x86-64 assembly using an intermediate representation and manual memory management. | 1,836 |