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

Certified Programming with Dependent Types

adamc@69:

Adam Chlipala

adamc@39: adamc@39:
adamc@39:

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.

adamc@39:
adamc@39: adamc@39:
adamc@226:

Distribution Formats

adamc@39: adamc@226:
adamc@226: adamc@226:
adamc@226:

Used by:

adamc@226: adamc@226:
adamc@226: adamc@226:
adamc@226:

Status

adamc@226: adamc@226:

Updated on November 16, 2009 with a version retargeted to Coq 8.2pl1. 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 (practical aspects of) CIC metatheory and axioms; a chapter on best practices with dependent De Bruijn syntax; some examples of locally nameless syntax; more examples of Ltac design patterns; discussion of tactic debugging and maintenance.

adamc@39:
adamc@39: adamc@39: