## 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:

- an old Tutorial, which is a commented interactive session which introduces basics on terms, proofs, and tactics (Gérard Huet, Gilles Kahn and Christine Paulin-Mohring).
- Coq in a Hurry (Yves Bertot, 2006);
- a Tutorial on Recursive Types in Coq (Eduardo Giménez, Pierre Castéran, 2006) and the associated examples;
- Video tutorials (Andrej Bauer, 2011);
- A Gentle Introduction to Type Classes and Rewriting in Coq (Pierre Castéran, Matthieu Sozeau, 2012) and the associated examples for Coq 8.3-8.5;
- Preuves de programmes en coq (Video lectures in French) (Yves Bertot, 2013);
- a tutorial browsable interactively as a Coq file (Mike Nahas, 2014);
- Videos of the DeepSpec Summer School 2017, introducing Coq and many advanced uses;

Other documentation

Some additional ressources:

- a bunch of Frequently Asked Questions;
- Cocorico!, the Coq wiki;
- index of internal, developer-oriented documentation of Coq's source code;
- odoc generated documentation of Coq's API for the development version of Coq;
- reference manual for the development version of Coq;
- documentation of the standard library for the development version of Coq.