8th out of 30 books — 18 voters
Goodreads helps you keep track of books you want to read.
Start by marking “Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant” as Want to Read:
Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant
The technology of mechanized program verification can play a supporting role in many kinds of research projects in computer science, and related tools for formal proof-checking are seeing increasing adoption in mathematics and engineering. This book provides an introduction to the Coq software for writing and checking mathematical proofs. It takes a practical engineering ...more
Hardcover, 424 pages
Published December 6th 2013 by MIT Press (MA)
(first published February 3rd 2010)
To see what your friends thought of this book, please sign up.
Jun 19, 2014 Nick Black marked it as to-read
Recommended to Nick by: Simon Thompson
Heard good things about this from numerous people within Google and beyond. I haven't looked at theorem proving software or proof assistants in over a decade, probably, and only really played with HOL4 back then (despite one of the world's authorities on the subject, Mary Jean Harrold, being at Georgia Tech...alas).
Excellent book, though a bit difficult to follow in places. You should also be prepared to look in the Coq manual a lot, or work with another book in parallel, as some things aren't explained in great detail, only showed in practices. This isn't such a big obstacle though, since the Coq manual works well in those cases.
Goodreads is hiring!
If you like books and love to build cool products, we may be looking for you.
Learn more »
Learn more »