[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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.