[TYPES/announce] Print release of a textbook on the Coq proof assistant
adamc at csail.mit.edu
Fri Dec 13 13:50:16 EST 2013
I'd like to announce the availability in print of my book on the Coq
proof assistant, "Certified Programming with Dependent Types" ("CPDT").
The publisher is MIT Press, and you can find more information (including
links to order online) on my site for the book:
Here's a quick summary of what this book is about and why the TYPES
crowd may be interested.
Computer proof assistant programs support machine-checked mathematical
proofs in almost any domain. The most popular applications of such
tools include program verification and proofs in programming language
metatheory; and Coq is one of the most popular proof assistants today
for those applications. CPDT is meant as a first-principles
introduction to Coq, assuming background knowledge that most readers of
this mailing list will have (experience with statically typed functional
programming and understanding of a few of the core ideas in, e.g.,
Pierce's "Types and Programming Languages").
Of course, while machine-checked proofs sound great in theory, in
practice many researchers (not to mention practitioners) shy away from
them because of the effort required to convince the proof-checking
program of interesting theorems. CPDT is oriented toward teaching
engineering practices to minimize friction in implementing,
understanding, and maintaining large formal proof developments. I hope
the toolbox it provides is enough to lower the overhead of machine
formalization to the point where, for your next conference paper, it is
easier to machine-check the proofs than to convince yourself that you've
done them right on paper.
What particular strategies does the book focus on? Broadly, they are
programming with dependent types and programming with Coq's
domain-specific language for proof search. The former makes it possible
to "prove" many interesting theorems just by writing more detailed type
annotations on functional programs, without any extra step of "writing
proofs." The latter makes it possible to write one proof search program
that, if all goes well, will do completely automatic proof of all
related theorems in a family, all versions of a theorem as its statement
evolves in the course of a project, etc. In all cases, we remain able
to check proofs in a trustworthy way, via type-checking for a relatively
simple lambda calculus.
I'm grateful to MIT Press for agreeing to this experiment where I may
continue distributing free versions of the book online.
More information about the Types-announce