Documentation

Reference documentation

The Coq development team maintains the following reference documents:

  • the Reference Manual, which is the complete, authoritative source of documentation for Coq;
  • the documentation of the Standard Library distributed with the system.

A PDF version of the reference manual can be downloaded from the the release page on GitHub.

Note that this reference documentation is not a good place to start using Coq. See below for more appropriate documentation for beginners.

Books and long tutorials

The following books and long tutorials were written by experienced Coq users and teachers:

  • Coq'Art, the first book dedicated to the Coq proof assistant (Yves Bertot, Pierre Castéran, 2004, Chinese version in 2009), only the French version and the exercises can be downloaded for free, English version is available on Springer's website;
  • Software Foundations, a series of Coq-based textbooks on logic, functional programming and foundations of programming languages (Benjamin Pierce et al, 2007, with regular updates), much acclaimed for being accessible to beginners, but rather oriented to computer scientists;
  • Certified Programming with Dependent Types, a textbook about practical engineering with Coq (Adam Chlipala, 2008), teaches advanced practical tricks and a very specific style of proof;
  • Program Logics for Certified Compilers, (Andrew W. Appel et al., 2014), a book that explains how to construct powerful and expressive program logics using the theory of separation logic, accompanied by a formal model in Coq, the Verified Software Toolchain, which is applied to the C light programming language and other examples.
  • Formal Reasoning About Programs (Adam Chlipala, 2017), a book that simultaneously provides a general introduction to formal logical reasoning about the correctness of programs and to using Coq for this purpose.
  • Programs and Proofs, (Ilya Sergey, 2017), a book that gives a brief and practically-oriented introduction to the basic concepts of interactive theorem proving using Coq; emphasizes the computational nature of inductive reasoning about decidable propositions via a small set of primitives from the SSreflect proof language.
  • Computer Arithmetic and Formal Proofs, (S. Boldo and G. Melquiond, 2017), a book that gives a comprehensive view of how to formally specify and verify tricky floating-point algorithms with Coq using the Flocq library.
  • the Mathematical Components book (A. Mahboubi and E. Tassi, 2018), a book that is more oriented towards mathematically inclined users, to dive into Coq with the SSReflect proof language, and the Mathematical Components library.
Shorter tutorials and videos

The following provide shorter introductions to Coq or specific topics, and may be targetted to beginners or more advanced users:

Other documentation

Some additional ressources: