Certified Programming with Dependent Types

by Adam Chlipala

The author trying to convince readers that the technology of program verification is mature enough today that it makes senes to use it in a support role in many kinkds of research projects in computer science. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation.

This book is generated automatically from Coq (format proof managment system) source files. The lastest PDF version is available at: http://adam.chlipala.net/cpdt/cpdt.pdf

Genres: Computer Science, Programming, Mathematics, Nonfiction, Textbooks

369 pages, ebook

First published February 3, 2010

Reviews

[Nick Black]

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 · Rating 5 out of 5]

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 · Rating 4 out of 5]

Very clear and informative book about Coq and dependent types. Requires some background in those areas, though.