<html><head><linkrel="stylesheet"type="text/css"href="/style.css"><title>Certified Programming with Dependent Types</title></head><body><h1>Certified Programming with Dependent Types</h1>
<divclass="summary"><p>This is the web site for an in-progress textbook about practical engineering with <ahref="http://coq.inria.fr/">the Coq proof assistant</a>. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation.</p><p>This is the text for a <ahref="http://www.cs.harvard.edu/~adamc/cpdt/">Fall 2008 class at Harvard</a>.</p></div><divclass="project"><ul><li><ahref="cpdt.pdf">Latest draft as a PDF</a></li><li><ahref="html/toc.html">Online version of latest draft, as hyperlinked HTML</a></li><li><ahref="cpdt.tgz">Tarball of Coq source to latest draft</a></li></div></body></html>