annotate staging/index.html @ 308:d092baf477ae

New release
author Adam Chlipala <>
date Thu, 25 Aug 2011 14:55:38 -0400
parents 20c742997dae
children 8cb9e31f86e7
rev   line source
adamc@39 1 <html>
adamc@39 2 <head>
adamc@268 3 <link rel="alternate" type="application/rss+xml" title="Updates RSS Feed" href="updates.rss">
adamc@39 4 <link rel="stylesheet" type="text/css" href="/style.css">
adamc@39 5 <title>Certified Programming with Dependent Types</title>
adamc@39 6 </head><body>
adamc@39 7 <h1>Certified Programming with Dependent Types</h1>
adamc@69 8 <h2><a href="">Adam Chlipala</a></h2>
adamc@39 9
adamc@39 10 <div class="summary">
adamc@39 11 <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@267 12
adamc@267 13 <p>I'm following an unusual philosophy in this book, so it may be of interest even to long-time Coq users. At the same time, I hope that it provides an easier introduction for newcomers, since short and automated proofs are the starting point, rather than an advanced topic.</p>
adamc@267 14
adamc@267 15 <p>The final part of the book applies the earlier parts' tools to examples in programming languages and compilers.</p>
adamc@267 16
adamc@270 17 <p>Interested in beta testing this book in a course you're teaching? Please <a href="">drop me a line</a>!</p>
adam@299 18
adam@299 19 <p>A traditional hardcopy version will appear from <a href="">MIT Press</a> Real Soon Now.</p>
adamc@39 20 </div>
adamc@39 21
adamc@39 22 <div class="project">
adamc@226 23 <h2>Distribution Formats</h2>
adamc@39 24 <ul>
adamc@39 25 <li> <a href="cpdt.pdf">Latest draft as a PDF</a></li>
adamc@39 26 <li> <a href="html/toc.html">Online version of latest draft, as hyperlinked HTML</a></li>
adamc@39 27 <li> <a href="cpdt.tgz">Tarball of Coq source to latest draft</a></li>
adamc@268 28 <li> <a href="updates.rss">RSS feed of updates</a></li>
adamc@226 29 </ul>
adamc@226 30 </div>
adamc@226 31
adamc@226 32 <div class="project">
adamc@226 33 <h2>Used by:</h2>
adamc@226 34 <ul>
adam@308 35 <li>6.892 at MIT <a href="">(Fall 2011)</a></li>
adam@308 36 <li>CS252 at Harvard <a href="">(Fall 2008)</a></li>
adamc@226 37 </ul>
adamc@226 38 </div>
adamc@226 39
adamc@226 40 <div class="project">
adamc@226 41 <h2>Status</h2>
adamc@226 42
adam@308 43 <p>Updated on November 16, 2009 with a version retargeted to Coq 8.2pl1, and then again on January 14, 2011 to support Coq 8.3. On August 25, 2011, I've started passes through all chapters, with an eye toward getting ready both for <a href="">my fall class</a> and publication by MIT Press. I'm adding bibliographic references, index entries, and additional exercises, along with the usual tweaks and improvements.</p>
adamc@231 44
adamc@266 45 <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 46
adamc@266 47 <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@267 48
adam@308 49 <p>My current tentative plan is to separate out the final part, on programming languages and compilers, into a distinct, online-only document, but I might be persuaded otherwise.</p>
adamc@39 50 </div>
adamc@39 51
adamc@39 52 </body></html>