Yves Bertot from INRIA Pierre Castéran from the Université of Bordeaux wrote the book Interactive Theorem Proving and Program Development, Coq'Art: the calculus of inductive constructions, the first book on practical uses of the Coq system, a system for computer-assisted proof developed at INRIA and the University of Paris-South.
This book is now available as a volume of the series Text in theoretical computer science: an EATCS series published by Springer-Verlag in may 2004. Its complete description is:
Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions Series: Texts in Theoretical Computer Science. An EATCS Series Bertot, Yves, Castéran, Pierre 2004, XXV, 469 p., Hardcover ISBN: 3-540-20854-2
This site gives access to an extensive collection of exercises in English, with their corrections. The exercises can be used in combination with the book or independently.
Yves Bertot de l'INRIA et Pierre Castéran de l'Université de Bordeaux sont heureux de vous présenter le Interactive Theorem Proving and Program Development, Coq'Art: The Calculus of Inductive Constructions, le premier livre sur l'utilisation du système Coq, un système de démonstration sur ordinateur développé à l'INRIA et à l'université de Paris-Sud.
Ce livre fournit une introduction progressive aux concepts les plus novateurs du système Coq, en les décrivant à l'aide de nombreux exemples et exercices. Les problèmes les plus couramment rencontrés par les utilisateurs avancés du système sont également abordés et des solutions sont décrites.
Ce livre est donc conçu pour les étudiants désireux de faciliter leurs premiers contacts avec ce système de démonstration, pour les enseignants qui veulent diffuser l'utilisation du calcul des constructions dans les méthodes formelles et pour les professionnels (chercheurs ou ingénieurs) qui veulent en maîtriser toute la puissance.
Le site associé fournit les scripts d'exemples utilisés dans le livre, les sujets et les corrections de tous les exercices (sauf les plus simples).
Ce livre est publié chez Springer-Verlag et nous invitons à le commander dans votre bibliothèque favorite.