Coq

Links

UniMath - Coq library aims to formalize a substantial body of mathematics using the univalent point of view.

Mathematical Components - Libraries of formalized mathematics developed using the Coq proof assistant. (GitHub)

Programs and Proofs - Lecture notes for a short course on proving/programming in Coq via SSReflect.

Kami - DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness.

Formal Reasoning About Programs - In-progress, open-source book by Adam Chlipala simultaneously introducing the Coq proof assistant and techniques for proving correctness of programs. (HN) (Web) (MIT course)

Alectryon - Library to process Coq snippets embedded in documents, showing goals and messages for each Coq sentence.

Cerise - Formalisation of a capability machine and principles for reasoning about security properties.

Bits - Formalization of bitset operations in Coq with a corresponding axiomatization and extraction to OCaml native integers.

Example of Coq Plugin using Dune - Contains a template for writing a Coq plugin using the Dune build system.

Eliminating Reflection from Type Theory - Coq formalisation of a translation from (an) extensional type theory to (a) weak type theory.

Last modified 6d ago

Copy link