## 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 (Yves Bertot and Pierre Castéran, 2004, Chinese version in 2009), the first book dedicated to the Coq proof assistant, only the French version and the Coq source and exercises can be downloaded for free, an English version is available from Springer's website.
- Software
Foundations (Benjamin Pierce
*et al.*, 2007, with regular updates), a series of Coq-based textbooks on logic, functional programming and foundations of programming languages , much acclaimed for being accessible to beginners, but rather oriented to computer scientists. - Certified Programming with Dependent Types (Adam Chlipala, 2008), a textbook about practical engineering with Coq, 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 Clight 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 (Sylvie Boldo and Guillaume 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.
- Mathematical Components (Assia Mahboubi and Enrico 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.
- Hydras & Co.
(Pierre Castéran
*et al.*, 2021–present), Continuously in-progress book on Kirby and Paris' hydra battles and other entertaining formalized mathematics in Coq, including library code and exercises.

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:

- contributing guide;
- 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).