Types Summerschool
C. Paulin-Mohring & J.-C. Filliâtre
Bertinoro-august 2007
Course 1-2
Inductive definitions
slides
Course 3
Introduction to
Coq
slides
Coq-lab
Exercises for Tuesday
Exercise on streams (file to be completed)
Demos
Sources files
Resources
Tar file with all documents
Krakatoa
Updated version of Krakatoa
tar file of the sources
References
[1]
Yves Bertot and Pierre Castéran.
Interactive Theorem Proving and Program Development
. Springer-Verlag, 2004.
[2]
The Coq Development Team.
The Coq Proof Assistant Reference Manual – Version V8.1
, July 2006.
.
This document was translated from L
A
T
E
X by
H
E
V
E
A
.