Rocq-community
Repositories list
75 repositories
coq-nix-toolbox
Publiccoq-ext-lib
PublicA library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]docker-base
PublicParent image for Docker images of the Coq proof assistant [maintainer=@Justme0606]rocq-lsp
PublicVisual Studio Code Extension and Language Server Protocol for Rocq / Coq [maintainers=@gbdrt,@SkySkimmer,@tabareau]rocq-lean-import
Publicparamcoq
PublicOld Coq plugin for parametricity [maintainer=@ppedrot]run-coq-bug-minimizer
Publicautosubst
PublicAutomation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]docker-rocq
Publictrocq
PublicA modular parametricity plugin for proof transfer in Coq [maintainers=@CohenCyril,@ecranceMERCE,@amahboubi,@lweqx,@MysaaJava]micromega-plugin
Publiccoqeal
PublicThe Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]parseque
PublicTotal Parser Combinators in Coq [maintainer=@womeier]fourcolor
Publicgaia
PublicImplementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]tarjan
PublicCoq formalization of algorithms due to Tarjan and Kosaraju for finding strongly connected graph components using Mathematical Components and SSReflect [maintain…coq-performance-tests
PublicA library of Coq source files testing for performance regressions on Coq [maintainer=@JasonGross]math-classes
PublicA library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]corn
PublicCoq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]mmaps
PublicModular Finite Maps over Ordered Types in Coq [maintainers=@letouzey,@palmskog]awesome-coq
Publicreduction-effects
PublicA Coq plugin to add reduction side effects to some Coq reduction strategies [maintainers=@liyishuai,@JasonGross]apery
Publictopology
PublicGeneral topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]stalmarck
PublicCertified implementation in Coq of Stålmarck's algorithm for proving tautologies [maintainer=@palmskog]aac-tactics
PublicCoq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]buchberger
PublicVerified implementation in Coq of Buchberger's algorithm for computing Gröbner bases [maintainer=@palmskog]graph-theory
PublicGraph Theory [maintainers=@chdoc,@damien-pous]atbr
PublicCoq library and tactic for deciding Kleene algebras [maintainer=@tchajed]coq-dpdgraph
PublicBuild dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]
ProTip! When viewing an organization's repositories, you can use the
props. filter to filter by custom property.