Fwd: [compilers] The grand restart -- new Coq book, plus interactive presentations [this wednesday]

[Anton Burtsev]

Here is your second chance to understand program verification: we'll
restart our Coq study this week with a new, much simpler book, interactive
presentations, and proof excercises in class.

The book we're starting to read is:

 Software Foundations, Benjamin C. Pierce et al.
 http://www.cis.upenn.edu/~bcpierce/sf/

There are two main reasons for us to start a new book. First, we've got
stuck with a rather abstract Adam Chlipala's book -- after three weeks
of reading it, we decided we want a way more concrete understanding of
how to work with Coq. Second, we wanted to invite more people for the
seminar -- Coq is truly relevant tool for everyone who does language
research. We found that a number of people who attend static analysis
class are interested to join us with Coq -- so this is the time to do
that.

Since we plan to do interactive Coq presentations during the class, your
read load is rather light. You even have options: don't read anything at
all, just listen to the presentation, or, since the book is simple, and
we're moving slow, you are encouraged to read the chapters which are
presented before class.

You task for this Wednesday is:

 Basics: Functional Programming
 http://www.cis.upenn.edu/~bcpierce/sf/Basics.html

Ryan will do the first presentation.

Anton