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.

Reviewer: Valentin F. Goranko (Johannesburg)

##### MSC:

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 |