lvc
Compiler project
A compiler project that aims to formalize and verify the semantics of an intermediate language using Coq
LVC verified compiler
57 stars
6 watching
2 forks
Language: Coq
last commit: almost 8 years agocompilercompiler-designconstant-propagationcoqcoq-formalizationlvclvc-compilerregister-allocationregister-assignmentspillingssa-constructionverificationverified-compiler
Related projects:
| Repository | Description | Stars |
|---|---|---|
 certicoq/certicoq | 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. | 137 |
 absint/compcert | A formally verified compiler for a subset of C that generates code for multiple architectures. | 1,901 |
 mit-plv/rupicola | A toolkit for compiling functional programs into imperative code for performance-critical applications | 51 |
 mustafaquraish/cup | A simple, C-like programming language compiler written in Rust to learn the basics of compilers and language processing | 295 |
 cxxxr/valtan | A compiler that translates Common Lisp code into JavaScript | 243 |
 pa-ba/calc-comp | Formalizations of compiler design and virtual machine calculations in Coq | 30 |
 l1mey112/crepl | A compiler and interpreter for executing C code on the fly as it is typed. | 29 |
 nilfoundation/zkllvm | Compiles high-level programming languages into input for provable computations protocols. | 304 |
 yubrot/llrl | An experimental compiler for a Lisp-like programming language with a focus on self-hosting and compilation to LLVM backend. | 156 |
 huynhtrankhanh/coqcp | Verifying competitive programming solutions to catch errors and improve rigor through formal mathematical proof | 22 |
 exokomodo/daybreak | A compiler project to create an interpretable language that compiles to native C code | 10 |
 covscript/covscript | An open-source interpreter for a cross-platform programming language designed to make programming easier | 227 |
 vellvm/vellvm | A formal verification project of the LLVM compiler's semantics using Coq proof assistant. | 405 |
 saman-pasha/lcc | A Lisp-like compiler and toolset for writing C code with additional features | 26 |
 terrajobst/minsk | An implementation of a compiler in C# that showcases basic concepts of compiler construction and language tooling. | 1,072 |