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
Enlarge cover
Rate this book
Clear rating
Open Preview

Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant

4.17  ·  Rating Details ·  18 Ratings  ·  3 Reviews
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)
More Details... edit details

Friend Reviews

To see what your friends thought of this book, please sign up.

Reader Q&A

To ask other readers questions about Certified Programming with Dependent Types, please sign up.

Be the first to ask a question about Certified Programming with Dependent Types

Community Reviews

(showing 1-49)
filter  |  sort: default (?)  |  Rating Details
Nick Black
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).
Jakub
Jan 20, 2015 Jakub rated it it was amazing
Shelves: challenge-2015
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.
Marvin
Very clear and informative book about Coq and dependent types. Requires some background in those areas, though.
Ricky Elrod
Ricky Elrod rated it it was amazing
Jun 15, 2015
Ch0c0late
Ch0c0late rated it really liked it
Apr 12, 2016
Stuart
Stuart rated it liked it
Jul 15, 2014
Jonathan Day
Jonathan Day rated it really liked it
Apr 12, 2015
Thomas Sutton
Thomas Sutton rated it really liked it
Apr 10, 2015
Chetan
Chetan rated it it was amazing
Sep 25, 2013
Tony Sloane
Tony Sloane rated it really liked it
Dec 11, 2012
Ismail Kuru
Ismail Kuru rated it it was amazing
Apr 10, 2016
Yosuke
Yosuke rated it liked it
Sep 12, 2016
Miho
Miho rated it really liked it
Oct 10, 2016
Karl
Karl rated it it was amazing
Mar 09, 2013
Tim Thornton
Tim Thornton rated it really liked it
Oct 20, 2014
Matvey Aksenov
Matvey Aksenov rated it it was amazing
Nov 15, 2016
Jovany Agathe
Jovany Agathe rated it it was ok
Nov 26, 2016
Rob Sloan
Rob Sloan rated it it was amazing
Mar 12, 2016
Landon Fuller
Landon Fuller rated it really liked it
Sep 21, 2015
Andy Legkiy
Andy Legkiy marked it as to-read
Jan 27, 2012
Alex Ott
Alex Ott marked it as to-read
Jan 28, 2012
Kirill
Kirill marked it as to-read
Jan 28, 2012
Marvin
Marvin marked it as to-read
Jul 23, 2012
Ilya
Ilya marked it as to-read
May 05, 2013
Maxim Moiseev
Maxim Moiseev marked it as to-read
Oct 10, 2014
Vishal
Vishal is currently reading it
Jul 08, 2013
Omar
Omar marked it as to-read
Jul 23, 2013
Kiran
Kiran marked it as to-read
Jul 24, 2013
Bernd Schadei
Bernd Schadei marked it as to-read
Sep 12, 2013
Molla
Molla marked it as to-read
Sep 17, 2013
Mattias Lundell
Mattias Lundell marked it as to-read
Dec 13, 2013
Ramy
Ramy marked it as to-read
Dec 18, 2013
Ilya
Ilya marked it as to-read
Dec 25, 2013
Sathishkumar
Sathishkumar is currently reading it
Jan 01, 2014
Chris
Chris marked it as to-read
Jan 02, 2014
Chris
Chris marked it as to-read
Jan 03, 2014
Mark Gently
Mark Gently marked it as to-read
Sep 07, 2016
Donald Williams
Donald Williams marked it as to-read
Jan 27, 2014
Anderson  Silva
Anderson Silva marked it as to-read
Mar 30, 2014
Harmanas Chopra
Harmanas Chopra marked it as to-read
Dec 21, 2014
Vipin
Vipin marked it as to-read
Jun 22, 2014
Dmitry Malikov
Dmitry Malikov marked it as to-read
Jun 25, 2014
John
John added it
Jul 23, 2014
András Kovács
András Kovács is currently reading it
Jul 09, 2014
There are no discussion topics on this book yet. Be the first to start one »

Goodreads is hiring!

If you like books and love to build cool products, we may be looking for you.
Learn more »

Share This Book