We have recently made releases of several projects in Coq-community for Coq 8.9. All of these releases are available in the Coq OPAM repository with the indicated package names.
-
AAC Tactics, a plugin that provides tactics for rewriting universally quantified equations, modulo associative and possibly commutative operators (
coq-aac-tactics) -
Chapar, a framework for verification of causal consistency for distributed key-value stores and their clients (
coq-chapar) -
Lemma Overloading, libraries demonstrating design patterns for programming and proving with canonical structures (
coq-lemma-overloading) -
Stalmarck, a correctness proof of Stålmarck’s algorithm for proving tautologies (
coq-stalmarck) -
Binary Rational Numbers, a development of rational numbers as finite binary lists (
coq-qarith-stern-brocot) -
Huffman, a proof of the correctness of the Huffman coding algorithm (
coq-huffman)
We thank the original authors of these projects, and we also thank Coq developers and Coq-community contributors for assistance with development, documentation, and automation.
Coq-community is always looking for volunteers to help maintain projects. Please take a look at our open issues for some suggestions of tasks.