[TYPES/announce] Print release of a textbook on the Coq proof assistant

[Adam Chlipala]

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:
     http://adam.chlipala.net/cpdt/

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.