Coq'Art Home page
Coq'Art is the familiar name for the first book on the Coq
proof assistant and its underlying theory the
/Calculus of Inductive Constructions /, written by Yves Bertot
and Pierre
Castéran .
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
Look at Springer site
.
Some chapters from the book
* Table of contents
* A brief overview
* Infinite Objects and Proofs
* Foundations of Inductive Types
French Version
A french version of the book is available here
.
/Drawing "Oiseau de feu" by courtesy of Michel Mendès France/
Coq 8.1, 8.2, 8.3, 8.4, 8.5 ...
The examples and solutions of exercises of the book are available as
gzipped tar files :
* for coq8.1pl3
* for coq8.2
* for coq8.3
* for coq 8.4
* for coq 8.5
* for coq 8.6
* for coq 8.7
* for coq 8.9
Please inform us of any problem.
Sources and exercises from the book
This site contains the source of all examples and the solution of 170
over 200 exercises from the book. Some new exercises are still added to
this repository.
For each exercise, we give a solution as a Coq file, together with some
comments if the exercise is difficult, or if the solution presents some
methodological interest. Comments are welcome.
table of contents
.
*All the examples and solutions of the exercises are under licence*
Cecill-B .
Participation is welcome
Thank you in advance for any comment, alternate solution, or any way to
improve this site.
Errata
Some typos where found after the printing of the book. They are reported
chapter by chapter, after the sources and exercises (look at this index
).
Many thanks to Stefan Karrmann and Pierre Lescanne for all the remarks
they sent to us.
------------------------------------------------------------------------
All (for 8.2) in a single tar file (gunzipped)
All the
examples and exercises on this site are copyright Yves Bertot and Pierre
Castéran.
Tutorial on [Co]-inductive types in Coq (V8.1 beta)
Look at this page
Slides for Tsinghua University Coq Summer School
Click here
The Teaser (draft)
A set of contributions for teaching Coq (in preparation)
To download Coq
Coq site here
------------------------------------------------------------------------
*Mail : * /first name/./name/@labri.fr