6 Resources

The resources listed on this page are not required for the course, but may prove useful.

The main Coq web page includes links to the Reference Manual (in HTML and PDF format) and a description of the Standard Library. But be warned: Coq is a large, complex system, and we will be using only a small fraction of it. We will construct much of what we need from scratch (in a way compatible with the Standard Library). These manuals may help clarify concepts from the book or lectures but they may also lead you into quite thorny thickets.

The book "Interactive Theorem Proving and Program Development" (subtitled "Coq’Art: The Calculus of Inductive Constructions", and colloquially referred to as "Coq’Art") by Yves Bertot and Pierre Casteran (2004), is a bottom-up description of Coq and some of its uses. It looks quite different from Software Foundations (which starts somewhere in the middle and expands carefully in various directions), though the two eventually overlap to some extent. If you can read French, there is a PDF available online from Casteran’s Web page, but otherwise it is an expensive hardcover purchase, and recommended only if you are intrigued by Software Foundations and plan to investigate Coq in more detail.

The book Certified Programming with Dependent Types (available online) is probably best read after Software Foundations; it includes some introductory material covered at a rapid rate, but is mostly intended to take Coq users to the next level. The author has a book in development that covers some of the same ground as Software Foundations but again at a more rapid rate, with more automation.

Systems similar to Coq include Isabelle/HOL, Nuprl, Lean, and the dependently-typed programming languages Twelf, Agda, and Idris.

Possibly the biggest success in using Coq to produce certified software is the CompCert C compiler. The Mathematical Components project provides many tools and developments, including the SSReflect language. Another interesting and prominent use of Coq is in an effort by mathematicians to provide an alternative foundation for mathematics using Homotopy Type Theory. There was a graduate course on the subject taught in the Pure Mathematics department at UW in spring 2014.