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
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
Look at Springer site .
The book in chinese
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
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 .
Participation is welcome
Thank you in advance for any comment, alternate solution, or any way to
improve this site.
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)
Slides for Tsinghua University Coq Summer School
The Teaser (draft)
A set of contributions for teaching Coq (in preparation)
To download Coq
Coq site here
Mail : first firstname.lastname@example.org