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

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.