About
Coq-community is a project for a collaborative, community-driven effort for the long-term maintenance and advertisement of packages for the Coq proof assistant. The organization is run by volunteer Coq users. Everyone is welcome - you don’t need to be a very experienced Coq user to participate. See the contributing guide for more information on how to get involved.
Project Hosting
Repositories for Coq-related projects can be hosted in the Coq-community organization on GitHub whenever any of the following is the case:
- the project has become a collective work (several community members are actively working on it);
- the initial author has stopped maintaining the project and someone else is volunteering to do so;
- the initial author is still maintaining the project but they want to encourage other community members to participate in the maintenance and possibly take over (and the project is indeed raising interest from the community);
- the project is a library or tool of general interest and it makes sense to develop it collaboratively.
Once a project has joined Coq-community, community members collaborate to ensure:
- project package definitions are continuously published in Coq’s opam package index and other relevant venues;
- projects use best practices for automation (e.g., building and continuous integration) as the project and Coq itself evolves;
- projects provide rich metadata and documentation to enable application in other projects and in research.
More details can be found in the Coq-community manifesto, in particular on the process for proposing a new package.
Current Projects
Below is a categorized list of active projects currently hosted in Coq-community. A star ⭐ indicates that the project is recommended for (re)use, while a warning sign ⚠️ indicates that the project is experimental or for other reasons not currently recommended for (re)use. Independently of stars or warnings, a rooster 🐓 indicates that a project is part of the Coq Platform, a distribution of Coq together with many generally useful libraries, plugins and tools.
Automation
Documentation and Tutorials
- 100 famous theorems proved using Coq - Repository tracking the theorems that have been proved in Coq from a list of 100 famous theorems.
- Awesome Coq ⭐ - Curated list of awesome Coq libraries, plugins, tools, verification projects, and resources.
- Coq’Art - Coq code and exercises from the Coq’Art book.
- Coq Plugin Template - Template repository for writing Coq plugins using the Dune build system, showcasing some advanced features such as linking to an external library.
- Coq Program Verification Template - Template repository for program verification in Coq, showcasing reasoning on CompCert’s Clight language using the Verified Software Toolchain.
- Hoare Tutorial - Tutorial on reflecting in Coq the generation of Hoare proof obligations.
- Hydras & Co. ⭐ - Variations on Kirby and Paris’ hydra battles and other entertaining math in Coq, including the Gödel-Rosser 1st incompleteness theorem (collaborative, documented, includes exercises).
- Lemma Overloading - Libraries demonstrating design patterns for programming and proving with canonical structures in Coq.
- Rosetta stone of metaprogramming in Coq - Different examples of tactics, plugins, etc., implemented in different metaprogramming languages.
- Semantics - Survey of semantics styles, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation.
- Tricks in Coq ⭐ - Tips, tricks, and features in Coq that are hard to discover, including example code.
Interfaces
- Conceal for VSCode - Prettify symbols mode for the Visual Studio Code and VSCodium editors.
- coqdocjs - Collection of scripts to improve the HTML output of coqdoc.
- VsCoq Legacy - Backwards-compatible extension for the Visual Studio Code and VSCodium editors using Coq’s legacy XML protocol.
- VSCoq - Language server and extension for the Visual Studio Code and VSCodium editors.
Libraries
- ALEA - Coq library for reasoning on randomized algorithms.
- Almost Full ⚠️ - Coq development of almost-full relations, including the Ramsey Theorem, useful for proving termination.
- Autosubst - Coq library and tactics for parallel de Bruijn substitutions.
- Bits ⚠️ - Formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers.
- CoqEAL 🐓 - Framework to ease change of data representations in proofs.
- Coq ExtLib ⭐ 🐓 - Library of Coq definitions, theorems, and tactics.
- Dblib - Coq library for working with de Bruijn indices.
- Generic Environments - Library which provides an abstract data type of environments.
- Parseque - Total parser combinators library, port of agdarsec.
- RegLang ⭐ 🐓 - Regular language representations in Coq.
Plugins
- AAC Tactics ⭐ 🐓 - Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators.
- ATBR - Coq library and plugin tactic for deciding Kleene algebras.
- Bignums ⭐ 🐓 - Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library.
- coq-dpdpgraph 🐓 - Plugin and tools for obtaining dependencies between Coq objects (definitions, theorems) and produce graphs.
- Paramcoq 🐓 - Coq plugin for parametricity.
- Reduction Effects ⚠️ 🐓 - Plugin to add side effects to some Coq reduction strategies.
- Trocq ⚠️ - Modular parametricity plugin for proof transfer using univalence.
- coqffi - Tool for generating Coq FFI bindings to OCaml libraries.
- Proviola ⚠️ - Tool for reanimation of Coq proofs.
Type Theory and Mathematics
- Apery - Proof in Coq, by computer algebra, that the real number ζ(3), known as Apéry’s constant, is irrational.
- Binary Rational Numbers - Coq development of rational numbers as finite binary lists.
- Completeness and Decidability of Modal Logic Calculi - Constructive proofs of soundness and completeness for the modal logics K, K*, CTL, PDL, and PDL with converse.
- CoRN ⭐ 🐓 - Repository of constructive mathematics formalized in Coq, including the algebraic hierarchy and real calculus.
- Coqtail - Library of mathematical theorems and tools in Coq, ranging from arithmetic to real and complex analysis.
- Dedekind Reals - Formalization of the Dedekind real numbers in Coq.
- Exact real arithmetic ⚠️ - Exact real arithmetic in Coq.
- Four Color Theorem ⭐ - Formal proof in Coq of the Four Color Theorem, a landmark result in graph theory.
- Gaia ⭐ - Implementation of books from Bourbaki’s Elements of Mathematics in Coq.
- Graph Theory - Library of formalized graph theory results in Coq.
- High School Geometry - Geometry in Coq for French high school.
- Math Classes ⭐ 🐓 - Library of abstract interfaces for mathematical structures in Coq.
- Pocklington - Pocklington’s criterion for primality in Coq.
- Topology - General topology and set theory in Coq.
Verified Software
- Bertrand - Coq proof of Bertrand’s postulate on existence of primes, with an application to the correctness of Knuth’s algorithm for prime numbers.
- Buchberger - Verified implementation of Buchberger’s algorithm for computing Gröbner bases in Coq.
- Coqoban - Coq implementation of Sokoban, the Japanese warehouse keepers’ game.
- Chapar ⚠️ - Framework for verification of causal consistency for distributed key-value stores and their clients in Coq.
- Huffman ⭐ - Correctness proof of the Huffman coding algorithm in Coq.
- JMLCoq ⚠️ - Coq definition of JML and a verified runtime assertion checker.
- Modular Finite Maps over Ordered Types - Several implementations of finite maps over arbitrary ordered types using Coq functors, including using red-black trees and AVL trees.
- Regexp Brzozowski ⚠️ - Decision procedures in Coq for regular expression equivalence.
- Stalmarck - Verified implementation in Coq of Stålmarck’s algorithm for proving tautologies.
- Sudoku - Certified Sudoku solver in Coq.
- Tarjan and Kosaraju - Coq formalizations of algorithms originally due to Kosaraju and Tarjan for finding strongly connected components in finite graphs.
View Coq-community on GitHub