verified
Algorithmic library
A collection of formalized and provable data structures and algorithms in Coq for educational purposes
Coq formalizations and proofs of (data) structures and algorithms.
46 stars
4 watching
3 forks
Language: Coq
last commit: over 6 years ago coqformal-verification
Related projects:
| Repository | Description | Stars |
|---|---|---|
 coq-community/lemma-overloading | A Coq library demonstrating design patterns for automated proof automation and canonical structures | 26 |
 fblanqui/color | A comprehensive Coq library providing formal definitions and proofs of rewriting theory, lambda-calculus, and termination. | 35 |
 charguer/tlc | A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. | 38 |
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 442 |
| coq-community/alea | A library for reasoning about randomized algorithms in Coq | 25 |
 stepchowfun/proofs | A personal repository of formally verified mathematics using the Coq proof assistant | 291 |
 imdea-software/fcsl-pcm | Provides formalisation of Partial Commutative Monoids (PCMs) for verification of pointer-manipulating sequential and concurrent programs. | 26 |
| coq-community/fav-ssr | A comprehensive library of verified data structures and algorithms in Coq | 45 |
| coq-community/bits | A formalization of bitset operations in Coq with extraction to OCaml native integers. | 22 |
| coq-community/corn | A comprehensive formalization of mathematical structures and concepts for verified computation in Coq. | 111 |
| coq-community/coqeal | A Coq library providing algebraic data structures and algorithms | 66 |
| coq-community/comp-dec-modal | Machine-checked proofs of soundness, completeness, and decidability for modal logics in Coq. | 8 |
 ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
 unimath/unimath | Formalizes mathematics using the univalent point of view | 961 |
 certikos/coqrel | A Coq-based library for establishing logical relations in formal verification and proof assistance | 20 |