annotate staging/index.html @ 517:136d4b84eb96

Build an open-source release of library modules
author Adam Chlipala <>
date Thu, 05 Dec 2013 15:51:33 -0500
parents a8377999fcf9
children 2bd6b00f831f
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
adam@309 15 <p>Interested in beta testing this book in a course you're teaching? Please <a href="">drop me a line</a>!</p>
adam@299 16
adam@309 17 <p>A traditional hardcopy version will appear from <a href="">MIT Press</a> Real Soon Now<a href="">*</a>.</p>
adamc@39 18 </div>
adamc@39 19
adamc@39 20 <div class="project">
adamc@226 21 <h2>Distribution Formats</h2>
adamc@39 22 <ul>
adamc@39 23 <li> <a href="cpdt.pdf">Latest draft as a PDF</a></li>
adam@515 24 <li> <a href="html/toc.html">Online version of latest draft, as hyperlinked HTML</a> [note that the author focuses on the PDF version and doesn't make an effort to keep the HTML version particularly pleasant to use]</li>
adamc@39 25 <li> <a href="cpdt.tgz">Tarball of Coq source to latest draft</a></li>
adam@517 26 <li> <a href="cpdtlib.tgz">Tarball of a few generally useful library modules from the book</a> (which are released under an open-source license, while the book generally isn't)</li>
adam@321 27 <li> <a href="repo">Public, read-only Mercurial repository</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">
adam@489 33 <h2><a href="ex/">Online Collection of Exercises for the Book</a></h2>
adam@489 34 </div>
adam@489 35
adam@489 36 <div class="project">
adamc@226 37 <h2>Used by:</h2>
adamc@226 38 <ul>
adam@516 39 <li>EECS 395 at Northwestern <a href="">(Fall 2013)</a></li>
adam@481 40 <li>CIS 670 at Penn <a href="">(Fall 2012)</a></li>
adam@308 41 <li>6.892 at MIT <a href="">(Fall 2011)</a></li>
adam@308 42 <li>CS252 at Harvard <a href="">(Fall 2008)</a></li>
adamc@226 43 </ul>
adamc@226 44 </div>
adamc@226 45
adamc@226 46 <div class="project">
adamc@226 47 <h2>Status</h2>
adamc@226 48
adam@482 49 <p>Updated on November 16, 2009 with a version retargeted to Coq 8.2pl1, then again on January 14, 2011 to support Coq 8.3, and then again on March 29, 2012 to support Coq 8.4 beta. On August 25, 2011, I 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 added bibliographic references and index entries, along with the usual tweaks and improvements. In late Summer 2012, the mode switched to final proofreading by others.</p>
adamc@231 50
adamc@266 51 <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 52
adam@380 53 <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 (now only in a supplementary file), 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 54
adam@332 55 <p>Previous versions included a final Part on programming language semantics in particular. I have decided to separate that part out. I plan to put it up as a supplementary resource eventually; for now it is simply removed. (It remains present in the <a href="repo">Mercurial</a> history.)</p>
adamc@39 56 </div>
adamc@39 57
adamc@39 58 </body></html>