-
Notifications
You must be signed in to change notification settings - Fork 22
/
index.html
81 lines (67 loc) · 4.24 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en">
<head>
<meta charset="utf-8" />
<title>Coq'Art Examples and Exercises</title>
</head>
<body bgcolor="#08FFFF">
<img src="firebird.jpg" width="40%" align="right">
<h1>Coq'Art Examples and Exercises</h1>
Coq'Art is the familiar name for the first book on the
<a href="http://coq.inria.fr">Coq proof assistant</a> and its underlying
theory the <em>Calculus of Inductive Constructions</em>, written
by <a href="http://www-sop.inria.fr/members/Yves.Bertot/">Yves Bertot</a>
and <a href="https://www.labri.fr/perso/casteran/">Pierre Castéran</a>.
See <a href="https://www.springer.com/gp/book/9783540208549">Springer's book website</a>.
<pre>
Interactive Theorem Proving and Program Development
Coq'Art: The Calculus of Inductive Constructions
Series: Texts in Theoretical Computer Science. An EATCS Series
Bertot, Yves, and Castéran, Pierre
2004, XXV, 469 p., Hardcover
ISBN: 3-540-20854-2
DOI: 10.1007/978-3-662-07964-5
</pre>
The examples and exercises on this site are copyright Yves Bertot and Pierre Castéran, unless explicitely mentioned. The tutorial on type classes and user-defined relations was written by Pierre Castéran and Matthieu Sozeau. The tutorial on [co-]inductive type was written by Eduardo Giménez and Pierre Castéran. All material is available under the open-source <a href="https://opensource.org/licenses/MIT">MIT license</a>.
<br>
<br>
<em><font color="#DF0000">Drawing "Oiseau de feu" by courtesy of Michel Mendès France</font></em>
<h2>Contents</h2>
<h3>16 directories, each one associated with a chapter of the book</h3>
Each directory contains a list of exercises, and an adaptation to recent versions of Coq of
the scripts presented in the corresponding chapter of the book. Each index file contains
also corrections of the errors that were kindly signalled to us by the readers.
<ol>
<li> <a href="ch1_overview/index.html"> A Brief Presentation of Coq </a>
<li> <a href="ch2_types_expressions/index.html"> Gallina: Coq as a Programming Language </a>
<li> <a href="ch3_propositions_proofs/index.html"> Propositions and Proofs </a>
<li> <a href="ch4_dependent_product/index.html"> Dependent Product </a>
<li> <a href="ch5_everydays_logic/index.html"> Everyday logic </a>
<li> <a href="ch6_inductive_data/index.html"> Inductive Data Structures </a>
<li> <a href="ch7_tactics_automation/index.html"> Tactics and automation </a>
<li> <a href="ch8_inductive_predicates/index.html" > Inductive Predicates </a>
<li> <a href="ch9_function_specification/index.html" > Functions and their specification </a>
<li> <a href="ch10_extraction_and_imperative_programs/index.html" > Extraction and imperative programming </a>
<li> <a href="ch11_search_trees/index.html"> A Case Study: binary search trees </a>
<li> <a href="ch12_modules/index.html"> The Module System </a>
<li> <a href="ch13_co_inductive_types/index.html"> Infinite Objects and Proofs </a>
<li> <a href="ch14_fundation_of_inductive_types/index.html"> Foundations of Inductive Types </a>
<li> <a href="ch15_general_recursion/index.html"> General Recursion </a>
<li> <a href="ch16_proof_by_reflection/index.html"> Proof by reflection </a>
</ol>
<h3>Additional material</h3>
<ul>
<li><a href="tutorial_type_classes/index.html">Coq sources</a> associated with <a href="https://www.labri.fr/perso/casteran/CoqArt/TypeClassesTut/typeclassestut.pdf">the tutorial</a> written by Pierre Castéran and Matthieu Sozeau on type classes and user-defined relations
<li><a href="tutorial_inductive_co_inductive_types/index.html">Coq sources</a> associated with <a href="https://www.labri.fr/perso/casteran/RecTutorial.pdf">the tutorial</a> written by Eduardo Giménez and Pierre Castéran on inductive and co-inductive types
<li><a href="more_exercises/index.html">More exercises</a> (not in the book)
</ul>
<h2>Errata</h2>
Some typos were found after the printing of the book. They are reported
chapter by chapter, after the sources and exercises.
Many thanks to Stefan Karrmann for all the remarks he sent to us.
<h2>Comments are welcome</h2>
Comments, alternative solutions, and suggestions to improve this site are welcome
as issues and pull requests <a href="https://github.com/coq-community/coq-art">on GitHub</a>.
Thank you in advance!
</body>
</html>