# 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 .

A review by ACM Computing Reviews

*Drawing "Oiseau de feu" by courtesy of Michel Mendès France*
## New Exercises !

## 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.

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 .

## 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 for all the remarks he sent to us.

All 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.0)

## Coq Art Gallery

Look at this page
## To download Coq

Coq site here

** Mail : ** *first name*.*name*@labri.fr