[TYPES/announce] Alpha release of a book on program proof in Coq

[Adam Chlipala]

I'm writing to make an official announcement of a draft book that I've 
had online for a few months:
     http://adam.chlipala.net/frap/
I developed it this past spring in the context of a graduate course.  
There are a number of nontrivial improvement plans that I have queued up 
mentally, for the next few times I offer the course, but someone may 
find it useful in the mean time.

It's called "FRAP," for "Formal Reasoning About Programs."  Like 
Software Foundations, it tries to introduce both the Coq proof assistant 
and some classic techniques in semantics and program proof.  The pace is 
faster than in Software Foundations, so there's time to cover a broader 
range of topics, like model checking with abstraction, automated proofs 
in separation logic, reasoning about concurrent programs with shared 
memory or message passing, etc. (Actually, that pace still needs some 
adjustment to properly serve an audience jumping in without much 
formal-methods experience!)  One distinguishing characteristic of the 
book is phrasing (almost) everything in terms of transition systems and 
their invariants, to expose commonalities across approaches.

The book runs in parallel with a PDF using classic math notation and 
with Coq source files mechanizing all the results.  It's released under 
a Creative Commons license.  I have exercises that I assigned in the 
first related course offering, though some of them deserve significant 
reconfiguration for difficulty level and so on.

Brave souls might consider using (parts of) the book already, and I'm 
glad to receive suggestions.