Thursday, January 07, 2010

Certified Programming with Dependent Types

By Adam Chlipala,
http://adam.chlipala.net/cpdt/

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.

No comments: