Yves Bertot de l'INRIA et Pierre Castéran de l'Université de Bordeaux sont heureux de vous présenter le Coq'Art, 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.
Pour l'instant le livre est accessible électroniquement en suivant ce lien.
La version courante est la version 1.386 portant la date (année/mois/jour) suivante:
2003/02/04