CompCert

Similar projects

Found by comparing what the projects do, not just their names.

• certicoq/certicoq137

  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.

• pa-ba/calc-comp30

  Compiler formalism

  Formalizations of compiler design and virtual machine calculations in Coq

• inria/velus63

  Lustre compiler

  A formally verified compiler for the Lustre programming language

• jscert/jscert196

  JavaScript verifier

  A Coq-based verification of the ECMAScript 5 standard for a JavaScript interpreter

• sigurdschneider/lvc57

  Compiler project

  A compiler project that aims to formalize and verify the semantics of an intermediate language using Coq

• certicoq/veriffi39

  Verification library

  Enables verified interaction between Coq programs and C libraries

• l1mey112/crepl29

  Compiler

  A compiler and interpreter for executing C code on the fly as it is typed.

• hackerfoo/poprc244

  Recursive language compiler

  A compiler for a language that supports recursion and concatenative data structures with features like dependent types and partial evaluation

• c2lang/c2compiler703

  C compiler

  A C compiler written in the C2 language itself.

• jserv/amacc1K

  Compiler

  A compiler for the Arm architecture that compiles a subset of C to generate executables and supports just-in-time execution.

• cpitclaudel/company-coq351

  Coq IDE

  An Emacs plugin that enhances Coq mode with various features and tools for writing and debugging proof-based software

• vexu/arocc1.2K

  C compiler

  A compiler written in Zig to translate C code into machine-specific binary code

• querycert/qcert56

  Compiler framework

  A framework for developing and verifying domain-specific languages with a focus on compiler correctness and verification.