adamc@39: adamc@39: adamc@268: adamc@39: adamc@39: Certified Programming with Dependent Types adamc@39: adamc@39:

Certified Programming with Dependent Types

adamc@69:

Adam Chlipala

adamc@39: adam@518:
adam@518: book cover adam@518: adam@518:

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.

adamc@267: adamc@267:

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.

adamc@267: adam@518:

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

adam@299: adam@518:

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!

adam@518: adam@518:

Buy a Copy in Print

adam@518: adamc@39:
adamc@39: adamc@39:
adam@518:

Distribution Formats (free version)

adamc@39: adamc@226:
adamc@226: adamc@226:
adam@489:

Online Collection of Exercises for the Book

adam@489:
adam@489: adam@489:
adam@526:

Use in classes

adam@526: adam@557:

Classes where CPDT is/was a primary text

adamc@226: adam@526: adam@526:

Classes where CPDT is/was a supplementary text

adam@526: adam@526: adam@526:

Reading groups

adam@526: adamc@226:
adamc@226: adamc@226:
adam@518:

Old versions

adamc@267: adam@332:

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

adamc@39:
adamc@39: adam@570:


adam@570:

One scholar appreciating the book

adam@570: adam@553: adam@553: adamc@39: