GitPlanet

Cheap and reliable Node.js hosting starts at $3/month, and $1/month static HTML hosting

Created with love in Canada, visit hostnodejs.com today

Feel like to post an Ad? Learn Details
All Projects → AbsInt → Compcert

AbsInt / Compcert

Licence: other
The CompCert formally-verified C compiler

Programming Languages

c
50402 projects - #5 most used programming language

Labels

compilercoq

Projects that are alternatives of or similar to Compcert

Coq Of Ocaml
Import OCaml programs to Coq 🐓 🐫
Stars: ✭ 117 (-88.11%)
Mutual labels:  compiler, coq
Certicoq
A Verified Compiler for Gallina, Written in Gallina
Stars: ✭ 66 (-93.29%)
Mutual labels:  compiler, coq
Ferret
Ferret is a free software lisp implementation for real time embedded control systems.
Stars: ✭ 878 (-10.77%)
Mutual labels:  compiler
Paramcoq
Coq plugin for parametricity [[email protected]]
Stars: ✭ 32 (-96.75%)
Mutual labels:  coq
Sml Compiler
A compiler for Standard ML, somewhat
Stars: ✭ 22 (-97.76%)
Mutual labels:  compiler
Hello World
A Hello World program in Coq.
Stars: ✭ 14 (-98.58%)
Mutual labels:  coq
Hott
Homotopy type theory
Stars: ✭ 946 (-3.86%)
Mutual labels:  coq
Ledgertheory
Stars: ✭ 12 (-98.78%)
Mutual labels:  coq
Mooncraft
Lua to Commandblock compiler
Stars: ✭ 33 (-96.65%)
Mutual labels:  compiler
Rum
💀 Compiler for the Rum language
Stars: ✭ 21 (-97.87%)
Mutual labels:  compiler
Nuprlincoq
Implementation of Nuprl's type theory in Coq
Stars: ✭ 31 (-96.85%)
Mutual labels:  coq
Asl
Arma Scripting Language - a clean scripting language compiling to Arma 3 SQF scripts.
Stars: ✭ 20 (-97.97%)
Mutual labels:  compiler
Vvclocks
Verified vector clocks, with Coq!
Stars: ✭ 14 (-98.58%)
Mutual labels:  coq
Write A Programming Language
How to make a new language(and why we shouldn't?)
Stars: ✭ 29 (-97.05%)
Mutual labels:  compiler
Jt89
sn76489an compatible Verilog core, with emphasis on FPGA implementation and Megadrive/Master System compatibility
Stars: ✭ 14 (-98.58%)
Mutual labels:  coq
Zion
A statically-typed strictly-evaluated garbage-collected readable programming language.
Stars: ✭ 33 (-96.65%)
Mutual labels:  compiler
Kaleidoscope
Haskell LLVM JIT Compiler Tutorial
Stars: ✭ 870 (-11.59%)
Mutual labels:  compiler
Rexjs
Rexjs is a faster and smaller JavaScript(ES6+) compiler!
Stars: ✭ 15 (-98.48%)
Mutual labels:  compiler
Wasp
A programming language that understands what a web app is.
Stars: ✭ 940 (-4.47%)
Mutual labels:  compiler
Rustiny
A Rust-like language compiling to x86-64 assembler
Stars: ✭ 34 (-96.54%)
Mutual labels:  compiler
View All Similar Projects ➔

CompCert

The formally-verified C compiler.

Overview

The CompCert C verified compiler is a compiler for a large subset of the C programming language that generates code for the PowerPC, ARM, x86 and RISC-V processors.

The distinguishing feature of CompCert is that it has been formally verified using the Coq proof assistant: the generated assembly code is formally guaranteed to behave as prescribed by the semantics of the source C code.

For more information on CompCert (supported platforms, supported C features, installation instructions, using the compiler, etc), please refer to the Web site and especially the user's manual.

License

CompCert is not free software. This non-commercial release can only be used for evaluation, research, educational and personal purposes. A commercial version of CompCert, without this restriction and with professional support and extra features, can be purchased from AbsInt. See the file LICENSE for more information.

Copyright

The CompCert verified compiler is Copyright Institut National de Recherche en Informatique et en Automatique (INRIA) and AbsInt Angewandte Informatik GmbH.

Contact

General discussions on CompCert take place on the [email protected] mailing list.

For inquiries on the commercial version of CompCert, please contact [email protected]

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].