[TYPES/announce] New draft textbook on practical Coq

[Adam Chlipala]

I would like to announce the first complete beta version of a draft 
textbook that I'm working on, available online under a Creative Commons 
license:
     http://adam.chlipala.net/cpdt/

This text deals with practical engineering with the Coq proof assistant 
(http://coq.inria.fr/), a tool for building machine-checked mathematical 
proofs. The focus is on building programs with proofs of correctness, 
using dependent types and scripted proof automation.

I'm following an unusual philosophy in this book, so it may be of 
interest even to long-time Coq users. At the same time, I hope that it 
provides an easier introduction for newcomers, since short and automated 
proofs are the starting point, rather than an advanced topic.  If you've 
been waiting for a little push to learn how to machine-check your proofs 
about languages and logics, this book may provide part of that push. :)

The final part of the book applies the earlier parts' tools to examples 
in programming languages and compilers.

I'm very interested in hearing from people who might like to beta test 
this book in courses that they're teaching.  There are a few exercises 
already in the book, with more probably to come, and I have a non-public 
set of sample solutions to those that are already included.