fiat
Data type synthesizer
A Coq-based library for synthesizing correct-by-construction abstract data types and parsers from formal specifications
Mostly Automated Synthesis of Correct-by-Construction Programs
149 stars
9 watching
32 forks
Language: Coq
last commit: almost 2 years agoLinked from 1 awesome list
coq-community/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
| mit-plv/fiat-crypto | Automated generation of cryptographic primitive code using a constructive design approach | 723 |
| mit-plv/coqutil | A collection of reusable tools and utilities for working with the Coq proof assistant | 42 |
| mit-plv/riscv-coq | An implementation of the RISC-V instruction set specification in Coq | 110 |
| mit-plv/bedrock | Automated verification of higher-order programs using separation logic | 57 |
| mit-plv/bbv | A repository unifying bit vector definitions and lemmas across multiple Coq projects. | 27 |
| mit-plv/kami | A platform for high-level parametric hardware specification and modular verification | 143 |
| mit-plv/rupicola | A toolkit for compiling functional programs into imperative code for performance-critical applications | 51 |
| mit-plv/koika | A formal language for designing and verifying rule-based hardware systems | 143 |
 lexifi/lrt | A package providing runtime type representations and a syntax extension to synthesize them from OCaml types | 32 |
 fblanqui/color | A comprehensive Coq library providing formal definitions and proofs of rewriting theory, lambda-calculus, and termination. | 35 |
 rafaelcgs10/w-in-coq | A Coq formalization of Damas-Milner type system and its algorithm W for verifying the correctness of type inference tools. | 25 |
 dboulytchev/minikanren-coq | A certified semantics for relational programming language specification, providing verified implementations of syntax and semantics for miniKanren languages | 26 |
 matafou/libhyps | A Coq library providing tactics to manipulate hypotheses in formal proofs. | 20 |
 plclub/lngen | Tool for generating Coq definitions and proofs for locally nameless representations | 30 |
| mit-plv/riscv-semantics | A formal specification of the RISC-V instruction set architecture in Haskell | 159 |