Certified Programming with Dependent Types

Adam Chlipala

book cover

This is the web site for a textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation.

I'm following an unusual philosophy in this book, so it may be of interest even to long-time Coq users. At the same time, I hope that it provides an easier introduction for newcomers, since short and automated proofs are the starting point, rather than an advanced topic.

Interested in using this book in a course you're teaching? Please drop me a line!

A traditional hardcopy version is available from MIT Press, who have graciously agreed to allow distribution of free versions online indefinitely, minus the benefits of the Press' copy editing!

Buy a Copy in Print

Distribution Formats (free version)

Online Collection of Exercises for the Book

Use in classes

Classes where CPDT is/was a primary text

Classes where CPDT is/was a supplementary text

Reading groups

Old versions

Previous versions included a final Part on programming language semantics in particular. I have decided to separate that part out. I plan to put it up as a supplementary resource eventually; for now it is simply removed. (It remains present in the Mercurial history.)

One scholar appreciating the book