Certified Programming with Dependent Types

Adam Chlipala

This is the web site for an in-progress 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.

This is the text for a Fall 2008 class at Harvard.