Lambda the Ultimate

For a few years now, I've been working on a textbook introducing the Coq proof assistant. It's been available freely online, and I'd like to announce now the availability of a print version from MIT Press. The site I've linked to includes links to order the book online.

Quick context on why LtUers might be interested in Coq: it supports machine checking of mathematical proofs, including in program verification and PL metatheory, some of the most popular applications of proof assistant technology.

Quick context on what distinguishes this book from other Coq resources: it focuses on the engineering techniques to develop large formal developments effectively. It turns out that there are some reusable lessons on how to write formal proofs so that they tend to continue to work even when theorem statements change over the courses of projects.

I'm grateful to MIT Press for agreeing to this experiment where I may continue distributing free versions of the book online.