AAC Tactics, a plugin that provides tactics for rewriting universally quantified equations, modulo associative and possibly commutative operators (
Chapar, a framework for verification of causal consistency for distributed key-value stores and their clients (
Lemma Overloading, libraries demonstrating design patterns for programming and proving with canonical structures (
Stalmarck, a correctness proof of Stålmarck’s algorithm for proving tautologies (
Binary Rational Numbers, a development of rational numbers as finite binary lists (
Huffman, a proof of the correctness of the Huffman coding algorithm (
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.