alea
Randomized algorithms reasoner
A library for reasoning about randomized algorithms in Coq
Coq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@volodeyka]
25 stars
3 watching
0 forks
Language: Coq
last commit: about 4 years ago
Linked from 2 awesome lists
coqmonadpaper-artifactsprobabilityrandomized-algorithms
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
| coq-community/lemma-overloading | A Coq library demonstrating design patterns for automated proof automation and canonical structures | 26 |
| coq-community/coqeal | A Coq library providing algebraic data structures and algorithms | 67 |
| coq-community/fav-ssr | A comprehensive library of verified data structures and algorithms in Coq | 45 |
 affeldt-aist/monae | A Coq library for formalizing and reasoning about monads with equational logic | 70 |
| coq-community/tarjan | Formalization of Tarjan and Kosaraju's strongly connected component algorithm in Coq for finite graphs. | 13 |
| coq-community/gaia | A Coq implementation of mathematical concepts from N. Bourbaki's Elements of Mathematics | 30 |
| 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/platform | A multi-platform distribution of the Coq proof assistant and its libraries, providing a standardized setup for development and teaching | 191 |
 jtassarotti/coq-proba | A Coq-based probability theory library providing results and definitions for discrete probability, measure theory, and probabilistic choice monads. | 50 |
| coq-community/atbr | A Coq library providing algebraic tools and tactics for working with binary relations | 23 |
 hivert/coq-combi | An algebraic combinatorics library formalized in Coq, providing a comprehensive set of functions and theories for symmetric functions. | 1 |
 ejgallego/pycoq | Python bindings for Coq's interactive proof assistant | 50 |
| coq-community/bits | A formalization of bitset operations in Coq with extraction to OCaml native integers. | 22 |
 verse-lab/ceramist | A verified hash-based approximate membership structure library in Coq | 121 |