Rocq-community

All

75 repositories

paramcoq
Public
Old Coq plugin for parametricity [maintainer=@ppedrot]
coq coq-plugin parametricity docker-coq-action coq-ci coq-platform
Rocq Prover
•
Other
•27•45•7•1•Updated Oct 3, 2025Oct 3, 2025
reduction-effects
Public
A Coq plugin to add reduction side effects to some Coq reduction strategies [maintainers=@liyishuai,@JasonGross]
coq side-effects coq-plugin coq-ci
Makefile
•
Mozilla Public License 2.0
•7•7•4•0•Updated Oct 3, 2025Oct 3, 2025
coq-ext-lib
Public
A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
library programming coq coq-ci coq-platform
Rocq Prover
•
BSD 2-Clause "Simplified" License
•51•136•19•3•Updated Oct 2, 2025Oct 2, 2025
aac-tactics
Public
Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]
coq coq-plugin coq-tactic docker-coq-action nix-action coq-ci coq-platform
OCaml
•
Other
•24•34•5•5•Updated Sep 30, 2025Sep 30, 2025
coq-nix-toolbox
Public
Nix helper scripts to automate local builds and CI [maintainers=@CohenCyril,@Zimmi48]
coq nix
Nix
•
MIT License
•19•46•31•7•Updated Sep 29, 2025Sep 29, 2025
run-coq-bug-minimizer
Public
Repository for triggering runs of the Coq bug minimizer using GitHub Actions [maintainer=@JasonGross]
Shell
•
MIT License
•0•2•10•0•Updated Sep 29, 2025Sep 29, 2025
corn
Public
Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]
coq coq-library real-number coq-ci coq-platform
Rocq Prover
•
GNU General Public License v2.0
•46•115•7•1•Updated Sep 28, 2025Sep 28, 2025
math-classes
Public
A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]
coq mathematics typeclasses coq-library coq-ci coq-platform
Rocq Prover
•
MIT License
•43•167•10•1•Updated Sep 28, 2025Sep 28, 2025
huffman
Public
Correctness proof of the Huffman coding algorithm in Coq [maintainer=@palmskog]
ocaml coq huffman-coding huffman-tree coq-extraction docker-coq-action coq-nix-toolbox
Coq
•
Other
•4•14•0•2•Updated Sep 28, 2025Sep 28, 2025
docker-rocq
Public
Docker images of the Rocq Prover (see also: https://github.com/rocq-community/docker-coq-action) [maintainers=@erikmd]
Dockerfile
•
MIT License
•0•2•4•2•Updated Sep 27, 2025Sep 27, 2025
rocq-lean-import
Public
OCaml
•
GNU Lesser General Public License v2.1
•8•24•4•1•Updated Sep 25, 2025Sep 25, 2025
apery
Public
A formal proof of the irrationality of zeta(3), the Apéry constant [maintainer=@amahboubi,@pi8027]
ssreflect mathcomp coq
Rocq Prover
•
Other
•8•25•5•0•Updated Sep 16, 2025Sep 16, 2025
coqeal
Public
The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
coq refinement mathcomp coq-ci coq-platform mathcomp-ci
Rocq Prover
•
Other
•17•72•6•3•Updated Sep 12, 2025Sep 12, 2025
trocq
Public
A modular parametricity plugin for proof transfer in Coq [maintainers=@CohenCyril,@ecranceMERCE,@amahboubi,@lweqx]
coq parametricity
Rocq Prover
•
GNU Lesser General Public License v3.0
•10•26•15•6•Updated Sep 12, 2025Sep 12, 2025
bits
Public
A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
bitset coq-library ssreflect paper-artifacts coq-extraction coq mathcomp
Rocq Prover
•
Apache License 2.0
•7•24•3•0•Updated Sep 7, 2025Sep 7, 2025
graph-theory
Public
Graph Theory [maintainers=@chdoc,@damien-pous]
coq graph-theory mathcomp docker-coq-action mathcomp-ci
Rocq Prover
•4•39•2•1•Updated Sep 4, 2025Sep 4, 2025
coq-dpdgraph
Public
Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]
dependency-analysis dependency-graph docker-coq-action coq-ci coq-platform coq
Rocq Prover
•
GNU Lesser General Public License v2.1
•32•93•11•10•Updated Sep 3, 2025Sep 3, 2025
awesome-coq
Public
A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainer=@palmskog]
awesome coq resources awesome-list
Creative Commons Zero v1.0 Universal
•25•360•5•1•Updated Aug 18, 2025Aug 18, 2025
docker-base
Public
Parent image for Docker images of the Coq proof assistant [maintainers=@erikmd]
coq docker-coq
Dockerfile
•
BSD 3-Clause "New" or "Revised" License
•4•4•1•1•Updated Aug 16, 2025Aug 16, 2025
coq-performance-tests
Public
A library of Coq source files testing for performance regressions on Coq [maintainer=@JasonGross]
testing performance coq
Coq
•
MIT License
•7•8•1•4•Updated Aug 12, 2025Aug 12, 2025
semantics
Public
A survey of semantics styles in Coq, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation [maintainer=@k4rtik]
coq programming-language-semantics
Rocq Prover
•
MIT License
•4•54•1•0•Updated Jul 31, 2025Jul 31, 2025
bignums
Public
Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]
large-numbers coq-plugin docker-coq-action coq-ci coq-platform coq
Rocq Prover
•
GNU Lesser General Public License v2.1
•22•25•1•1•Updated Jul 29, 2025Jul 29, 2025
parseque
Public
Total Parser Combinators in Coq [maintainer=@womeier]
parser-combinators coq
Rocq Prover
•
MIT License
•6•46•2•0•Updated Jul 19, 2025Jul 19, 2025
fourcolor
Public
Formal proof of the Four Color Theorem [maintainer=@ybertot]
ssreflect four-color-theorem mathcomp coq-ci coq
Rocq Prover
•
Other
•23•218•0•2•Updated Jul 5, 2025Jul 5, 2025
gaia
Public
Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]
coq set-theory ssreflect mathcomp docker-coq-action bourbaki mathcomp-ci
Rocq Prover
•
MIT License
•7•31•0•1•Updated Jun 27, 2025Jun 27, 2025
coq-100-theorems
Public
Statements of famous theorems proven in Coq [maintainer=@jmadiot]
coq theorems
HTML
•
Other
•15•60•2•2•Updated Jun 23, 2025Jun 23, 2025
templates
Public
Templates for configuration files and scripts useful for maintaining Coq projects [maintainers=@liyishuai,@palmskog,@Zimmi48]
continuous-integration coq mustache-templates
Mustache
•
The Unlicense
•10•16•23•4•Updated Jun 19, 2025Jun 19, 2025
tarjan
Public
Coq formalization of algorithms due to Tarjan and Kosaraju for finding strongly connected graph components using Mathematical Components and SSReflect [maintainers=@CohenCyril,@palmskog]
coq tarjan-algorithm ssreflect mathcomp mathcomp-ci
Rocq Prover
•
Other
•8•18•0•0•Updated Jun 17, 2025Jun 17, 2025
coq-performance-tests-plots-history
Public
Maintaining plot history for coq-community/coq-performance-tests gh-pages branch [maintainer=@JasonGross]
0•0•1•0•Updated Jun 1, 2025Jun 1, 2025
rocq-tricks
Public
Tricks you wish the Coq manual told you [maintainer=@tchajed]
coq
Coq
•
MIT License
•24•530•6•1•Updated May 28, 2025May 28, 2025