Interactive theorem proving and program development. Coq’Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring. (English) Zbl 1069.68095

Texts in Theoretical Computer Science. An EATCS Series. Berlin: Springer (ISBN 3-540-20854-2/hbk). xxv, 469 p. (2004).
Coq provides a proof development environment based on the calculus of inductive constructions, a type-theoretic logical framework. The tool is used for the formal verification of mathematical theorems and the development of certified programs. This book serves as a Coq user manual, supporting both beginners and experts in the use of Coq and its underlying theory. Throughout the book the theoretical development is interleaved with examples that the reader may interactively follow in Coq. Numerous exercises further enhance the utility as a learning aid. A supporting website provides downloadable source for all the examples and solutions to the exercises. As an introduction to Coq the book is self-contained, though some acquaintance with the typed \(\lambda\)-calculus and a corresponding functional language like ML would be recommended. The book is also comprehensive, including thorough coverage of advanced aspects of the system, though sections and exercises requiring higher competence have a graduated labelling. In summary, the book is an essential companion for every Coq user that will contribute to the accessibility and popularity of the Coq system.


68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
03B15 Higher-order logic; type theory (MSC2010)
03B35 Mechanization of proofs and logical operations
03B70 Logic in computer science
68N18 Functional programming and lambda calculus
68Q60 Specification and verification (program logics, model checking, etc.)
68-01 Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science


HOL; LEGO; PVS; Nuprl; ML ; Automath; Coq