Mercurial > cpdt > repo
annotate staging/index.html @ 229:2bb1642f597c
Prop section
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Fri, 20 Nov 2009 11:02:26 -0500 |
| parents | 9d0b9577f8b1 |
| children | bc0f515a929f |
| rev | line source |
|---|---|
| adamc@39 | 1 <html> |
| adamc@39 | 2 <head> |
| adamc@39 | 3 <link rel="stylesheet" type="text/css" href="/style.css"> |
| adamc@39 | 4 <title>Certified Programming with Dependent Types</title> |
| adamc@39 | 5 </head><body> |
| adamc@39 | 6 <h1>Certified Programming with Dependent Types</h1> |
| adamc@69 | 7 <h2><a href="http://adam.chlipala.net/">Adam Chlipala</a></h2> |
| adamc@39 | 8 |
| adamc@39 | 9 <div class="summary"> |
| adamc@39 | 10 <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> |
| adamc@39 | 11 </div> |
| adamc@39 | 12 |
| adamc@39 | 13 <div class="project"> |
| adamc@226 | 14 <h2>Distribution Formats</h2> |
| adamc@39 | 15 <ul> |
| adamc@39 | 16 <li> <a href="cpdt.pdf">Latest draft as a PDF</a></li> |
| adamc@39 | 17 <li> <a href="html/toc.html">Online version of latest draft, as hyperlinked HTML</a></li> |
| adamc@39 | 18 <li> <a href="cpdt.tgz">Tarball of Coq source to latest draft</a></li> |
| adamc@226 | 19 </ul> |
| adamc@226 | 20 </div> |
| adamc@226 | 21 |
| adamc@226 | 22 <div class="project"> |
| adamc@226 | 23 <h2>Used by:</h2> |
| adamc@226 | 24 <ul> |
| adamc@226 | 25 <li> CS252 at Harvard <a href="http://www.cs.harvard.edu/~adamc/cpdt/">(Fall 2008)</a></li> |
| adamc@226 | 26 </ul> |
| adamc@226 | 27 </div> |
| adamc@226 | 28 |
| adamc@226 | 29 <div class="project"> |
| adamc@226 | 30 <h2>Status</h2> |
| adamc@226 | 31 |
| adamc@226 | 32 <p>Updated on November 16, 2009 with a version retargeted to Coq 8.2pl1. 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 (practical aspects of) CIC metatheory and axioms; a chapter on best practices with dependent De Bruijn syntax; some examples of locally nameless syntax; more examples of Ltac design patterns; discussion of tactic debugging and maintenance.</p> |
| adamc@39 | 33 </div> |
| adamc@39 | 34 |
| adamc@39 | 35 </body></html> |