ceramist
Hash filter library
A verified hash-based approximate membership structure library in Coq
Verified hash-based AMQ structures in Coq
121 stars
7 watching
5 forks
Language: Coq
last commit: almost 5 years ago
Linked from 2 awesome lists
amqbloom-filtercoqcoq-formalizationcounting-bloom-filterprobabilityquotient-filter
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
 coq-community/fav-ssr | A comprehensive library of verified data structures and algorithms in Coq | 45 |
| verse-lab/toychain | A minimalistic blockchain-based consensus protocol implemented in Coq | 111 |
| coq-community/alea | A library for reasoning about randomized algorithms in Coq | 25 |
| coq-community/coqeal | A Coq library providing algebraic data structures and algorithms | 67 |
| coq-community/corn | A comprehensive formalization of mathematical structures and concepts for verified computation in Coq. | 111 |
| coq-community/atbr | A Coq library providing algebraic tools and tactics for working with binary relations | 23 |
| coq-community/parseque | A Coq library that provides a total parser combinator library with support for building parsers and grammars in the language of Coq. | 42 |
| coq-community/lemma-overloading | A Coq library demonstrating design patterns for automated proof automation and canonical structures | 26 |
| coq-community/bits | A formalization of bitset operations in Coq with extraction to OCaml native integers. | 22 |
| coq-community/topology | Develops and formalizes basic concepts and results of general topology in Coq. | 47 |
 stepchowfun/proofs | A personal repository of formally verified mathematics using the Coq proof assistant | 292 |
| coq-community/reglang | Provides definitions and verified translations between various representations of regular languages in the Coq proof assistant | 41 |
| coq-community/chapar | A framework for verifying causal consistency in distributed key-value stores and their clients using the Coq proof assistant | 32 |
| coq-community/autosubst | Automates formalizing syntactic theories with variable binders in Coq | 52 |
 pi8027/stablesort | Provides a modular and canonical way to prove the correctness of stable sorting algorithms in Coq. | 22 |