User loginNavigation 
Print release of a textbook on the Coq proof assistantFor 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. By Adam Chlipala at 20131213 18:57  LtU Forum  previous forum topic  next forum topic  other blogs  12640 reads

Browse archivesActive forum topics 
Recent comments
2 days 7 hours ago
2 days 9 hours ago
3 days 5 hours ago
3 days 12 hours ago
3 days 15 hours ago
3 days 16 hours ago
3 days 18 hours ago
4 days 9 hours ago
4 days 13 hours ago
1 week 21 hours ago