forked from coq/coq.github.io
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathdocumentation.html
245 lines (183 loc) · 8.85 KB
/
documentation.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
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
<#include "incl/macros.html">
<#def TITLE>Documentation</#def>
<#include "incl/header.html">
<div class="framework">
<div class="frameworklabel">Reference documentation</div>
<div class="frameworkcontent">
<p>The Coq development team maintains the following reference
documents:</p>
<ul>
<li>the <a href="/distrib/current/refman/">Reference Manual</a>, which
is the authoritative source of documentation for Coq. It
contains
a <a href="/distrib/current/refman/changes.html">changelog</a>
describing updates to Coq,
which we recommend you read when you upgrade Coq;</li>
<li>the documentation of
the <a href="/distrib/current/stdlib/">Standard Library</a> distributed
with the system.</li>
</ul>
<p>A PDF version of the reference manual can be downloaded from the
the <a href="https://github.com/coq/coq/releases/latest">release
page</a>.</p>
<p>Note that this reference documentation is not the recommended way to start
using Coq. See below for more appropriate documentation for beginners.</p>
</div>
<div class="frameworklinks">
<ul>
<li><a href="/distrib/current/refman/">Reference Manual</a></li>
<li><a href="/distrib/current/stdlib/">Standard Library</a></li>
<li><a href="/distrib/current/refman/changes.html">Changelog</a></li>
</ul>
</div>
</div>
<div class="framework">
<div class="frameworklabel">Books and long tutorials</div>
<div class="frameworkcontent">
<p>These books and long tutorials were written by experienced
Coq users and teachers:</p>
<ul>
<li><a href="https://www.labri.fr/perso/casteran/CoqArt/">Coq'Art</a>
(Yves Bertot and Pierre Castéran, 2004, Chinese version in 2009),
the first book dedicated to the Coq proof assistant, only the French
version and the
<a href="https://github.com/coq-community/coq-art">Coq source and
exercises</a> can be downloaded for free, an English version is available from
<a href="https://link.springer.com/book/10.1007/978-3-662-07964-5">Springer's
website</a>.</li>
<li><a href="https://softwarefoundations.cis.upenn.edu">Software
Foundations</a> (Benjamin Pierce <em>et al.</em>, 2007, with regular updates),
a series of Coq-based textbooks on logic, functional
programming and foundations of programming languages , much acclaimed for
being accessible to beginners, but rather oriented to computer
scientists.</li>
<li><a href="http://adam.chlipala.net/cpdt/">Certified Programming
with Dependent Types</a> (Adam Chlipala, 2008), a textbook about
practical engineering with Coq, teaches advanced practical tricks
and a very specific style of proof.</li>
<li><a href="https://www.cs.princeton.edu/~appel/papers/plcc.pdf">Program
Logics for Certified Compilers</a> (Andrew W. Appel <em>et al.</em>,
2014), a book that explains how to construct powerful and expressive
program logics using the theory of separation logic, accompanied by a
formal model in Coq,
the <a href="https://vst.cs.princeton.edu">Verified Software
Toolchain</a>, which is applied to the Clight programming language
and other examples.</li>
<li><a href="http://adam.chlipala.net/frap/">Formal Reasoning About
Programs</a> (Adam Chlipala, 2017), a book that simultaneously
provides a general introduction to formal logical reasoning about the
correctness of programs and to using Coq for this purpose.</li>
<li><a href="https://ilyasergey.net/pnp/">Programs and Proofs</a>
(Ilya Sergey, 2017), a book that gives a brief and
practically-oriented introduction to the basic concepts of interactive
theorem proving using Coq; emphasizes the computational nature of
inductive reasoning about decidable propositions via a small set of
primitives from the SSreflect proof language.</li>
<li><a href="http://iste.co.uk/book.php?id=1238">Computer Arithmetic
and Formal Proofs</a> (Sylvie Boldo and Guillaume Melquiond, 2017), a book that
gives a comprehensive view of how to formally specify and verify
tricky floating-point algorithms with Coq using the
<a href="https://gitlab.inria.fr/flocq/flocq">Flocq library</a>.</li>
<li><a href="https://math-comp.github.io/mcb/">Mathematical
Components</a> (Assia Mahboubi and Enrico Tassi, 2018), a book that is
more oriented towards mathematically inclined users, to dive into Coq
with the SSReflect proof language, and the Mathematical Components
library.</li>
<li><a href="https://github.com/uds-psl/MPCTT">Modeling and Proving in Computational Type Theory</a>
(Gert Smolka, 2021, with updates), a book covering topics in computational logic using Coq,
including foundations, canonical case studies, and practical programming.</li>
<li><a href="https://github.com/coq-community/hydra-battles">Hydras & Co.</a>
(Pierre Castéran <em>et al.</em>, 2021–present), continuously in-progress book on Kirby
and Paris' hydra battles and other entertaining formalized mathematics in Coq,
including library code and exercises.</li>
</ul>
</div>
<div class="frameworklinks">
<ul>
<li><a href="https://www.labri.fr/perso/casteran/CoqArt/">Coq'Art</a></li>
<li><a href="https://softwarefoundations.cis.upenn.edu">SF</a></li>
<li><a href="http://adam.chlipala.net/cpdt/">CPDT</a></li>
<li><a href="https://math-comp.github.io/mcb/">MCB</a></li>
</ul>
</div>
</div>
<div class="framework">
<div class="frameworklabel">Shorter tutorials and videos</div>
<div class="frameworkcontent">
<p>The following provide shorter introductions to Coq or specific
topics, and may be targeted to beginners or more advanced users:</p>
<ul>
<li><a href="https://cel.archives-ouvertes.fr/inria-00001173">Coq in a
Hurry</a> (Yves Bertot, 2006);</li>
<li>a <a href="http://www.labri.fr/perso/casteran/RecTutorial.pdf">Tutorial
on Recursive Types in Coq</a> (Eduardo Giménez, Pierre Castéran, 2006)
and the
<a href="https://github.com/coq-community/coq-art/blob/master/tutorial_inductive_co_inductive_types/SRC/RecTutorial.v">associated examples</a>;</li>
<li><a href="http://math.andrej.com/2011/02/22/video-tutorials-for-the-coq-proof-assistant/">Video
tutorials</a> (Andrej Bauer, 2011);</li>
<li><a href="http://www.labri.fr/perso/casteran/CoqArt/TypeClassesTut/typeclassestut.pdf">A
Gentle Introduction to Type Classes and Rewriting in Coq</a> (Pierre
Castéran, Matthieu Sozeau, 2012) and
the <a href="https://github.com/coq-community/coq-art/tree/master/tutorial_type_classes/SRC">associated
examples</a>;</li>
<li><a href="http://www-sop.inria.fr/members/Yves.Bertot/videos-coq/">Preuves
de programmes en coq</a> (Video lectures in French) (Yves Bertot,
2013);</li>
<li>a <a href="https://mdnahas.github.io/doc/nahas_tutorial">tutorial</a> browsable interactively
as a <a href="https://mdnahas.github.io/doc/nahas_tutorial.v">Coq file</a> (Mike Nahas,
2014);</li>
<li><a href="https://www.youtube.com/channel/UC5yB0ZRgc4A99ttkwer-dDw/feed">Videos</a>
of the DeepSpec Summer School 2017, introducing Coq and many advanced
uses;</li>
<li><a href="https://www.youtube.com/watch?v=5e7UdWzITyQ">Three-hour
video introduction of Coq</a> by Cody Roux at the Formal Methods for
the Informal Engineer workshop 2021.</li>
<li><a href="https://www.youtube.com/playlist?list=PLre5AT9JnKShFK9l9HYzkZugkJSsXioFs">Video lectures</a>
on Software Foundations by Michael Clarkson, with
<a href="https://github.com/clarksmr/sf-lectures">accompanying
material</a>.</li>
</ul>
</div>
<div class="frameworklinks">
<ul>
<li><a href="https://mdnahas.github.io/doc/nahas_tutorial">Mike Nahas's tutorial</a></li>
<li><a href="https://cel.archives-ouvertes.fr/inria-00001173">Coq in a Hurry</a></li>
</ul>
</div>
</div>
<div class="framework">
<div class="frameworklabel">Other documentation</div>
<div class="frameworkcontent">
<p>Some additional resources:</p>
<ul>
<li>a bunch
of <a href="https://github.com/coq/coq/wiki/The-Coq-FAQ">Frequently
Asked Questions</a>;</li>
<li><a href="https://github.com/coq/coq/wiki/">Cocorico!</a>, the Coq
wiki;</li>
<li>the <a href="https://www.codewars.com/?language=coq">Codewars
platform</a> hosts many challenges proposed by the community;</li>
</ul>
<p>Documentation for the version under development of Coq:</p>
<ul>
<li><a href="https://github.com/coq/coq/blob/master/CONTRIBUTING.md">contributing guide</a>;</li>
<li>index of internal,
developer-oriented <a href="https://github.com/coq/coq/tree/master/dev#miscellaneous-information-about-the-code-devdoc">documentation
of Coq's source code</a>;</li>
<li>odoc-generated <a href="https://coq.github.io/doc/master/api/">documentation
of Coq's API</a>;</li>
<li><a href="https://coq.github.io/doc/master/refman/">reference
manual</a> (version under development);</li>
<li><a href="https://coq.github.io/doc/master/stdlib/">documentation
of the standard library</a> (version under development).</li>
</ul>
</div>
<div class="frameworklinks">
<ul>
<li><a href="https://github.com/coq/coq/wiki/The-Coq-FAQ">F.A.Q.</a></li>
<li><a href="https://github.com/coq/coq/wiki/">Cocorico! (wiki)</a></li>
<li><a href="https://www.codewars.com/?language=coq">Codewars</a></li>
</ul>
</div>
</div>
<#include "incl/footer.html">