velus
Lustre compiler
A formally verified compiler for the Lustre programming language
A Lustre compiler in Coq
63 stars
10 watching
6 forks
Language: Coq
last commit: 12 months ago compcertcoq-formalizationlustresynchronous-language
Related projects:
| Repository | Description | Stars |
|---|---|---|
 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 |
 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 |
 coq-community/reglang | Provides definitions and verified translations between various representations of regular languages in the Coq proof assistant | 41 |
 reynir/brainfuck | Formalizing Brainfuck in Coq to prove its properties and verify a compiler for simple arithmetic expressions. | 26 |
 coq-concurrency/pluto | A Coq-based web server written in a functional programming language | 86 |
 sigurdschneider/lvc | A compiler project that aims to formalize and verify the semantics of an intermediate language using Coq | 57 |
| coq-community/fav-ssr | A comprehensive library of verified data structures and algorithms in Coq | 45 |
| coq-community/corn | A comprehensive formalization of mathematical structures and concepts for verified computation in Coq. | 111 |
 formal-land/coq-of-rust | Tool that verifies Rust code by translating it into Coq's proof system to ensure no bugs or vulnerabilities exist | 437 |
 jscert/jscert | A Coq-based verification of the ECMAScript 5 standard for a JavaScript interpreter | 196 |
| coq-community/gaia | A Coq implementation of mathematical concepts from N. Bourbaki's Elements of Mathematics | 30 |
 snu-sf/promising-coq | Development of a promising semantics for relaxed-memory concurrency | 33 |
 uwplse/cheerios | A formally verified serialization library for Coq | 23 |