To Coq or not to Coq? This impressive volume by Bertot and Castéran is a comprehensive introduction on the Coq system and its underlying theory. It presents an extensive and didactical overview of Gallina, Coq’s specification language, and Vernacular, its command language.

Coq was developed by teams that the authors were active parts of, over the past 30 or so years. It is presented as a powerful software environment that provides tools/tactics to construct proofs.

Based on Church’s &lgr;-calculus on the theoretical side, and the powerful objective Caml functional programming language, on the technical side, Coq is probably the most universal system in this problem area that one can now find; this must-have book is its tutorial. Using Coq to check programs against specifications, do proofs in higher-order logic, define our own formal systems and ask for proofs, is, to say the least, convenient.

The Coq v8 system (released in 2004) is a comfortable environment that embraces new advances in &lgr;-calculus and typing, called the calculus of inductive constructions, a variant of type theory.

The authors classify the 16 chapters into five groups: “The Calculus of Constructions” (chapters 2 through 5), “Inductive Constructions” (chapters 6 and 8), “Certified Programs and Extraction” (chapters 9 through 11), “Advanced Use” (chapters 12 through 15), and “Proof Automation” (chapters 7 and 16). The material is presented in an easy to follow fashion, and the authors provide all of the necessary background knowledge before attacking new ground. There is an abundance of examples, and problems to be solved by the reader. Some examples may look clumsy, and not too elegant at a first glance. That is done on purpose, apparently, as the mistakes made always underline a lesson to be remembered.

Two gurus in this problem domain, Gérard Huet and Christine Paulin-Mohring, provide a historic perspective on the development of Coq, and computational logic in general, in their lengthy introduction to this volume, which Springer published in its European Association for Theoretical Computer Science (EATCS) Series.

The bottom line is: yes to Coq, definitely. This is a great textbook.