Software Foundations. Benjamin C. Pierce et al.

For those that wonder what they're seeing, this book is about writing functional programs and proving them correct. This is done in the context of a dependently-typed language called Coq. An example of a dependent type is having a function that takes an integer value n and an array of size n as arguments and having the type system check that you call the function with a valid size and array at compile-time. It turns out that dependent types can be used in much more powerful ways, including proving deep correctness properties about programs (less powerful type systems (like Java's) are also "proofs", but the correctness properties they check are typically weaker).

There are video lectures with the author covering this book at a fast pace from this year's Oregon PL summer school (bottom of the page):

http://www.cs.uoregon.edu/Research/summerschool/summer12/cur...

I've read the first chapter and it's very good, I highly recommend working through the literate Coq files in Proof General, if you're familiar enough with Emacs. It's a pretty cool environment.

I haven't read this book, but Pierce's "Types and Programming Languages" is an absolutely fantastic introduction to type theory and programming language semantics.

The presentation of the book is also very innovative. The chapters are fairly short and to the point. There are chapters which discuss theory, then chapters which implement that theory in code.

folks will also want to check out Harper's (CMU) Practical Foundations for PL

http://www.cs.cmu.edu/~rwh/plbook/book.pdf