Nothing Special   »   [go: up one dir, main page]
Home

Documentation

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

Books and long tutorials

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.
  • Modeling and Proving in Computational Type Theory (Gert Smolka, 2021, with updates), a book covering topics in computational logic using Coq, including foundations, canonical case studies, and practical programming.
  • 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.
Shorter tutorials and videos

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

Other documentation

Some additional resources:

Documentation for the version under development of Coq: