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.
goedel
Archived since the contents have been moved to the Hydras & Co. repository
graph-theory
Graph Theory [maintainers=@chdoc,@damien-pous]
hoare-tut
A Tutorial on Reflecting in Coq the generation of Hoare proof obligations [maintainer=@k4rtik]
hydra-battles
Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
lemma-overloading
Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]
paramcoq
Coq plugin for parametricity [maintainer=@proux01]
reglang
Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]
semantics
A survey of semantics styles in Coq, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation [maintainer=@k4rtik]
sudoku
A certified Sudoku solver in Coq [maintainers=@siraben,@thery]
topology
General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]