Certified Programming with Dependent Types

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

From Amazon.com

The MIT Press page for the book

ISBN:

Distribution Formats (free version)

Latest draft as a PDF
Online version of latest draft, as hyperlinked HTML [note that the author focuses on the PDF version and doesn't make an effort to keep the HTML version particularly pleasant to use]
Tarball of Coq source to latest draft
Tarball of a few generally useful library modules from the book (which are released under an open-source license, while the book generally isn't)
Public, read-only Mercurial repository
RSS feed of updates

Online Collection of Exercises for the Book

Use in classes

Classes where CPDT is/was a primary text

CK0230 at Universidade Federal do Ceará (Fall 2017)
EECS 755 at U. Kansas (Fall 2017)
CS691PL at U. Mass. Amherst (Spring 2014)
CSE 506 at U. Washington (Winter 2014)
EECS 395 at Northwestern (Fall 2013)
CIS 670 at Penn (Fall 2012)
6.892 at MIT (Fall 2011)
CS252 at Harvard (Fall 2008)

Classes where CPDT is/was a supplementary text

ITP at U. Tübingen (Winter 2018/2019)
CS410 at Portland State (Fall 2018, Spring 2013)
CSI 5137 at U. Ottawa (Fall 2018)
6.822 at MIT (Spring 2018, Spring 2017, Spring 2016)
CS 6115 at Cornell (Fall 2017)
CS750 at IIT Kanpur (Fall 2017)
6.820 at MIT (Fall 2017, Fall 2015, Fall 2013)
CSCI 740 at RIT (Fall 2017)
CMSC631 at U. Maryland (Fall 2017)
CS260r at Harvard (Spring 2017)
CS250 at Harvard (Fall 2014)
CS 565 at Purdue (Spring 2014)
Formal Methods at UST China (Spring 2014)
185.A60 at TU Vienna (Spring 2014)
CMPS203 at UC Santa Cruz (Winter 2014)
CS 430 at Yale (Fall 2013)
IFT 6172 at U. Montreal (Spring 2013)
TIES341 at U. Jyväskylä (Spring 2013)
CMPT 340 at U. Saskatchewan (Spring 2012)
CS252r at Harvard (Fall 2011)
G54DTP at Nottingham (Spring 2011)
Formal Methods at U. Zagreb (Spring 2011)
CMPT 863 at U. Saskatchewan (Spring 2010)

Reading groups

CS 7190 at Cornell (Summer 2013)
At Radboud University Nijmegen (2010, 2016/2017)
At U. Wisconsin (2008-2009)

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.)