Mercurial > cpdt > repo
view staging/index.html @ 261:0a644d7004d5
New release
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Wed, 16 Dec 2009 17:31:57 -0500 |
parents | 621010c9522f |
children | aaf532c80729 |
line wrap: on
line source
<html> <head> <link rel="stylesheet" type="text/css" href="/style.css"> <title>Certified Programming with Dependent Types</title> </head><body> <h1>Certified Programming with Dependent Types</h1> <h2><a href="http://adam.chlipala.net/">Adam Chlipala</a></h2> <div class="summary"> <p>This is the web site for an in-progress textbook about practical engineering with <a href="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> </div> <div class="project"> <h2>Distribution Formats</h2> <ul> <li> <a href="cpdt.pdf">Latest draft as a PDF</a></li> <li> <a href="html/toc.html">Online version of latest draft, as hyperlinked HTML</a></li> <li> <a href="cpdt.tgz">Tarball of Coq source to latest draft</a></li> </ul> </div> <div class="project"> <h2>Used by:</h2> <ul> <li> CS252 at Harvard <a href="http://www.cs.harvard.edu/~adamc/cpdt/">(Fall 2008)</a></li> </ul> </div> <div class="project"> <h2>Status</h2> <p>Updated on November 16, 2009 with a version retargeted to Coq 8.2pl1. Last incremental update on December 16, 2009.</p> <p>Some chapters on programming languages and compilers are empty; these should be filled in soon-ish. Additional plans: a chapter on best practices with dependent de Bruijn syntax.</p> </div> </body></html>