[ The Types Forum (announcements only),
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
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.