Coq-community project releases for Coq 8.9

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.