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

Certified Programming with Dependent Types

adamc@39:

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:

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

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