## Documentation

The Coq development team maintains the following reference documents:

- the Reference Manual, which is the authoritative source of documentation for Coq. It contains a changelog describing updates to Coq, which we recommend you read when you upgrade 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.

Note that this reference documentation is not the recommended way to start using Coq. See below for more appropriate documentation for beginners.

These 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.

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

- 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;
- 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;
- Three-hour video introduction of Coq by Cody Roux at the Formal Methods for the Informal Engineer workshop 2021.

Some additional resources:

- a bunch of Frequently Asked Questions;
- Cocorico!, the Coq wiki;
- the Codewars platform hosts many challenges proposed by the community;

Documentation for the version under development of Coq:

- index of internal, developer-oriented documentation of Coq's source code;
- odoc-generated documentation of Coq's API;
- reference manual (version under development);
- documentation of the standard library (version under development).