The Coq Proof Assistant

Two main documents are officially maintained by the Coq development team:

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

Moreover, some users of Coq have published various documents that may be useful both to beginners and advanced users of Coq:

• the Coq'Art, the first book dedicated to the Coq proof assistant (Yves Bertot, Pierre Castéran, 2004, Chinese version in 2009);
• Software Foundations, a Coq-based textbook on logic, functional programming and foundations of programming languages (Benjamin Pierce et al, 2007, with regular updates);
• Certified Programming with Dependent Types, a textbook about practical engineering with Coq (Adam Chlipala, 2008);
• Video tutorials (Andrej Bauer, 2011);
• Preuves de programmes en coq (Video lectures in french) (Yves Bertot, 2013);
• Videos of the DeepSpec Summer School 2017, introducing Coq and many advanced uses;
• a tutorial browsable interactively as a Coq file (Mike Nahas, 2014);
• Coq in a Hurry (Yves Bertot, 2006);
• 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);
• a Tutorial on Recursive Types in Coq (Eduardo Giménez, Pierre Castéran, 2006) and the associated examples;
• a bunch of Frequently Asked Questions;
• Cocorico!, the Coq wiki;
• A Gentle Introduction to Type Classes and Rewriting in Coq (Pierre Castéran, Matthieu Sozeau, 2012) and the associated examples for Coq 8.3 and 8.4.