Following the renaming of the Coq proof assistant into the Rocq Prover, this organization has been renamed to Rocq-community.
Following the renaming of the Coq proof assistant into the Rocq Prover, this organization has been renamed to Rocq-community.
coqeal
The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
alea
Coq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@volodeyka]
chapar
A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]
bits
A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
vsc-conceal
Prettify Symbols Mode for Visual Studio Code [maintainer=@rtetley]
dedekind-reals
A formalization of the Dedekind real numbers in Coq [maintainer=@andrejbauer]
parseque
Total Parser Combinators in Coq [maintainer=@womeier]
aac-tactics
Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]
apery
A formal proof of the irrationality of zeta(3), the Apéry constant [maintainer=@amahboubi,@pi8027]
atbr
Coq library and tactic for deciding Kleene algebras [maintainer=@tchajed]