Sunday, January 10, 2010

Certified Programming with Dependent Types

Certified Programming with Dependent Types

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: