adamc@39: 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:Updated on November 16, 2009 with a version retargeted to Coq 8.2pl1. Last incremental update on December 11, 2009.
adamc@231: adamc@251: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.
adamc@39: