This repo is the new home of Proof General

Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]

Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]

Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]

Coq plugin for parametricity [maintainer=@proux01]

Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]

Graph Theory [maintainers=@chdoc,@damien-pous]

A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]

Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]

Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]

Archived since the contents have been moved to the Hydras & Co. repository

Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]

Correctness proof of the Huffman coding algorithm in Coq [maintainer=@palmskog]

Coq formalization of decision procedures for regular expression equivalence [maintainer=@anton-trunov]

Binary rational numbers in Coq [maintainer=@herbelin]

GitHub Action using Docker-Coq [maintainers=@erikmd,@Zimmi48]

Modular Finite Maps over Ordered Types in Coq [maintainers=@letouzey,@palmskog]

Verified implementation in Coq of Buchberger's algorithm for computing Gröbner bases [maintainer=@palmskog]

Coq development of almost-full relations, including the Ramsey Theorem, useful for proving termination [maintainer=@palmskog]

Coq definition of JML and a verified runtime assertion checker [maintainer=@palmskog]