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 2013-12-13 18:57 | LtU Forum | previous forum topic | next forum topic | other blogs | 14228 reads
|
Browse archives
Active forum topics |
Recent comments
20 weeks 1 day ago
20 weeks 1 day ago
20 weeks 1 day ago
42 weeks 2 days ago
46 weeks 4 days ago
48 weeks 1 day ago
48 weeks 1 day ago
50 weeks 6 days ago
1 year 3 weeks ago
1 year 3 weeks ago