[TYPES/announce] Alpha release of a book on program proof in Coq
adamc at csail.mit.edu
Fri Sep 2 16:46:51 EDT 2016
I'm writing to make an official announcement of a draft book that I've
had online for a few months:
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.
More information about the Types-announce