[TYPES/announce] Second announcement of an online book on program proof in Coq

[Adam Chlipala]

I'm writing to announce another "release" of my work-in-progress online 
book on program proof in Coq:
     http://adam.chlipala.net/frap/
It's called /Formal Reasoning About Programs//. /I've used it in two 
graduate classes so far, and I made another announcement about a year 
ago about an earlier version.  The current version is further tested and 
improved, including with new early tutorial material on Coq and with new 
chapters on data abstraction and compiler verification.

Some subscribers of this mailing list might want to consider running 
FRAP classes at their own institutions.  I think the book and associated 
materials are now well-enough developed to make that not a crazy idea, 
and I'm happy to provide personalized support in adapting the class to 
different settings.  Please do let me know if you're considering such an 
experiment.

In terms of educational goals, FRAP is a cousin to /Software 
Foundations/.  FRAP also aims to introduce Coq to a general 
computer-science audience, and it also aims to introduce classic 
semantics and program-proof techniques using Coq.  A crucial difference, 
though, is that FRAP assumes familiarity with topics like proof by 
induction -- which we generally "teach" to all CS undergraduates but, 
unfortunately, expect few to master.  Students need to be comfortable 
with both rigorous proofs and programming to keep up with FRAP, though 
they shouldn't need to come in with any experience in formal methods or 
functional programming.

The payoff from the higher starting expectations is getting through more 
of the PL canon.  I can testify that multiple students with no prior 
formal-methods experience have accomplished the following by the end of 
the class, taking a sampling of our assignments. (Admittedly, more such 
students drop the class than hang on to the end, but I'm still working 
on tweaking the "gentle on-ramp" aspect!)

  * Write mostly automated correctness proofs that a classic lock
    algorithm achieves mutual exclusion.
  * Verify a producer-consumer program by choosing a proper abstraction
    and then automatically model-checking the resulting system inside Coq.
  * Prove soundness of a logical relation and use it to demonstrate
    contextual equivalence of two implementations of a simple abstract
    data type.
  * Verify particular C-like programs using separation logic, with the
    level of proof automation we expect from standalone verification tools.
  * Prove that, in a shared-memory concurrent language, a global lock
    order avoids deadlock.
  * Prove soundness of rely-guarantee for shared-memory concurrent
    programs, and use it to verify example programs.

A nontrivial Coq library is behind the class, including both an 
alternative suite of basic tactics, to avoid some common beginner 
hang-ups; and a set of parameterized proof-automation engines, 
principally for model checking, abstract interpretation, and discharging 
verification conditions from separation logic.  Almost all the proof 
techniques in the class are cast in terms of the common formalism of 
state transition systems and their invariants, a commonality that I find 
isn't emphasized often enough in semantics classes.  (For instance, when 
we get to type soundness and the "progress and preservation" conditions 
behind the widely used syntactic approach, we see that they are just a 
special case of the principles of invariant induction and invariant 
strengthening that we have been using all along!)

I'll be very glad to hear from anyone interested in test-driving the 
material.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20170603/3bcf91ce/attachment.html>