Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Types Summerschool
[go: Go Back, main page]

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
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 LATEX by HEVEA.