FreeSpec
impure computation framework
A framework for specifying and verifying impure computations in a formal proof assistant
A framework for implementing and certifying impure computations in Coq
52 stars
9 watching
11 forks
Language: Coq
last commit: 10 months ago
Linked from 2 awesome lists
coqformal-verificationfreer-monads
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
 deepspec/interactiontrees | A library for representing recursive and impure programs in the Coq proof assistant language. | 203 |
 iu-parfunc/lvars | Provides a data structure and framework for monotonically-growing concurrent programs | 81 |
 stepchowfun/proofs | A personal repository of formally verified mathematics using the Coq proof assistant | 291 |
 imdea-software/htt | A verification system for reasoning about sequential heap-manipulating programs using separation logic and dependent types | 69 |
 ssprove/ssprove | A foundational framework for formalizing cryptographic proofs in Coq. | 56 |
 weakmemory/imm | Compilation correctness proofs for an intermediate memory model | 21 |
 adampetcher/fcf | A framework for machine-checked proofs of cryptography in the computational model. | 48 |
 coq-community/lemma-overloading | A Coq library demonstrating design patterns for automated proof automation and canonical structures | 26 |
| imdea-software/fcsl-pcm | Provides formalisation of Partial Commutative Monoids (PCMs) for verification of pointer-manipulating sequential and concurrent programs. | 26 |
 plsyssec/fact | A compiler for a constant-time programming language used in cryptography | 198 |
 nilfoundation/zkllvm | Compiles high-level programming languages into input for provable computations protocols. | 295 |
 foreverbell/verified | A collection of formalized and provable data structures and algorithms in Coq for educational purposes | 46 |
 magmide/magmide | Creating a programming language and ecosystem to make formal verification and provably correct software development practical and mainstream for working software engineers. | 812 |
 matafou/libhyps | A Coq library providing tactics to manipulate hypotheses in formal proofs. | 20 |
 lysxia/system-f | A formalization of polymorphic lambda calculus with a proof of parametricity theorem. | 33 |