annotate staging/index.html @ 266:43227e4b0b5c

First beta release
author Adam Chlipala <>
date Wed, 30 Dec 2009 13:47:59 -0500
parents aaf532c80729
children 8480a2517f19
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="">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="">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="">(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@266 32 <p>Updated on November 16, 2009 with a version retargeted to Coq 8.2pl1. Last incremental update on December 30, 2009.</p>
adamc@231 33
adamc@266 34 <p>The current version is effectively a beta release. It is intended to be consistent, self-contained, and useful, both for individual study and for introductory theorem-proving classes aimed at students with ML or Haskell experience and with basic familiarity with programming language theory.</p>
adamc@266 35
adamc@266 36 <p>The main omissions have to do with some supporting resources that I didn't get around to implementing when I used this book for a course. Some suggested exercises are present, but only at points where I was looking to assign an exercise in the course. Some chapters are lacking the annotations used to build reduced versions of their source code, where some definitions and proofs have been elided; the course instructor can step through such a file, guiding class participants in filling in the omitted code.</p>
adamc@39 37 </div>
adamc@39 38
adamc@39 39 </body></html>