coq-community

All

75 repositories

parseque
Public
Total Parser Combinators in Coq [maintainer=@womeier]
parser-combinators coq
Coq
•
MIT License
•6•43•2•0•Updated Mar 10, 2025Mar 10, 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•8•1•Updated Mar 3, 2025Mar 3, 2025
coq-nix-toolbox
Public
Nix helper scripts to automate local builds and CI [maintainers=@CohenCyril,@Zimmi48]
coq nix
Nix
•
MIT License
•12•37•29•4•Updated Mar 3, 2025Mar 3, 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 Mar 1, 2025Mar 1, 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•7•1•2•Updated Mar 1, 2025Mar 1, 2025
apery
Public
A formal proof of the irrationality of zeta(3), the Apéry constant [maintainer=@amahboubi,@pi8027]
ssreflect mathcomp coq
Coq
•
Other
•7•20•5•0•Updated Feb 28, 2025Feb 28, 2025
coqeal
Public
The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
coq refinement mathcomp coq-ci coq-platform mathcomp-ci
Coq
•
Other
•17•69•6•3•Updated Feb 28, 2025Feb 28, 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
Coq
•
MIT License
•7•30•0•0•Updated Feb 28, 2025Feb 28, 2025
fourcolor
Public
Formal proof of the Four Color Theorem [maintainer=@ybertot]
ssreflect four-color-theorem mathcomp coq-ci coq
Coq
•
Other
•22•193•0•3•Updated Feb 28, 2025Feb 28, 2025
paramcoq
Public
Old Coq plugin for parametricity [maintainer=@ppedrot]
coq coq-plugin parametricity docker-coq-action coq-ci coq-platform
Coq
•
Other
•24•45•6•2•Updated Feb 25, 2025Feb 25, 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
Coq
•
Other
•8•14•0•0•Updated Feb 25, 2025Feb 25, 2025
vscoq-legacy
Public
Legacy Visual Studio Code extension for Coq [maintainers=@huynhtrankhanh,@thery,@Blaisorblade]
TypeScript
•
MIT License
•1•1•4•0•Updated Feb 24, 2025Feb 24, 2025
aac-tactics
Public
Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]
coq-plugin coq-tactic docker-coq-action nix-action coq-ci coq-platform coq
OCaml
•
Other
•21•31•3•1•Updated Feb 21, 2025Feb 21, 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
Coq
•
GNU Lesser General Public License v2.1
•29•89•9•9•Updated Feb 19, 2025Feb 19, 2025
rocq-lean-import
Public
OCaml
•
GNU Lesser General Public License v2.1
•5•19•2•0•Updated Feb 19, 2025Feb 19, 2025
reglang
Public
Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]
regexp coq regular-languages ssreflect mathcomp docker-coq-action coq-nix-toolbox coq-platform mathcomp-ci
Coq
•
Other
•7•41•1•0•Updated Feb 16, 2025Feb 16, 2025
coq-art
Public
Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]
exercises coq-art docker-coq-action coq
Coq
•
MIT License
•24•117•1•1•Updated Feb 15, 2025Feb 15, 2025
graph-theory
Public
Graph Theory [maintainers=@chdoc,@damien-pous]
coq graph-theory mathcomp docker-coq-action mathcomp-ci
Coq
•4•36•2•1•Updated Feb 14, 2025Feb 14, 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
Coq
•
Apache License 2.0
•7•23•3•0•Updated Feb 14, 2025Feb 14, 2025
docker-coq
Public
Docker images of the Coq proof assistant (see also: https://github.com/coq-community/docker-coq-action) [maintainers=@erikmd,@himito]
ci coq opam docker-coq dockerfile docker-image
Dockerfile
•
BSD 3-Clause "New" or "Revised" License
•3•37•8•0•Updated Feb 13, 2025Feb 13, 2025
coq-tricks
Public
Tricks you wish the Coq manual told you [maintainer=@tchajed]
coq
Coq
•
MIT License
•22•515•5•0•Updated Feb 11, 2025Feb 11, 2025
trocq
Public
A modular parametricity plugin for proof transfer in Coq [maintainers=@CohenCyril,@ecranceMERCE,@amahboubi]
coq parametricity
Coq
•
GNU Lesser General Public License v3.0
•4•20•15•5•Updated Feb 10, 2025Feb 10, 2025
docker-base
Public
Parent image for Docker images of the Coq proof assistant [maintainers=@erikmd,@himito]
coq docker-coq
Dockerfile
•
BSD 3-Clause "New" or "Revised" License
•4•4•0•0•Updated Feb 10, 2025Feb 10, 2025
docker-rocq
Public
Docker images of the Rocq Prover (see also: https://github.com/coq-community/docker-coq-action) [maintainers=@erikmd,@himito]
Dockerfile
•
MIT License
•0•1•3•0•Updated Feb 10, 2025Feb 10, 2025
docker-coq-action
Public
GitHub Action using Docker-Coq [maintainers=@erikmd,@Zimmi48]
continuous-integration opam docker-coq container-ci docker-coq-action coq action github-actions
Shell
•
MIT License
•4•12•21•2•Updated Feb 9, 2025Feb 9, 2025
corn
Public
Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]
coq coq-library real-number coq-ci coq-platform
Coq
•
GNU General Public License v2.0
•45•113•8•1•Updated Jan 27, 2025Jan 27, 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
Coq
•
GNU Lesser General Public License v2.1
•22•22•1•1•Updated Jan 25, 2025Jan 25, 2025
hydra-battles
Public
Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
discrete-mathematics formal-proofs primitive-recursive-functions ordinal-notations docker-coq-action hydra-battles coq-nix-toolbox coq
Coq
•
MIT License
•12•73•7•5•Updated Jan 22, 2025Jan 22, 2025
coqoban
Public
Sokoban (in Coq) [maintainer=@erikmd]
puzzle coq-library coq
Coq
•
GNU Lesser General Public License v2.1
•2•21•1•0•Updated Jan 3, 2025Jan 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
•20•342•5•0•Updated Jan 2, 2025Jan 2, 2025