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.

Distribution Formats

Used by:

Status

Updated on November 16, 2009 with a version retargeted to Coq 8.2pl1. Last incremental update on December 9, 2009.

Some chapters on programming languages and compilers are empty or just contain Coq code; these should be filled in soon-ish. Additional plans: a chapter on best practices with dependent De Bruijn syntax; some examples of locally nameless syntax.