annotate staging/index.html @ 267:8480a2517f19

Mailing list announcement text expansion
author Adam Chlipala <>
date Wed, 06 Jan 2010 10:25:31 -0500
parents 43227e4b0b5c
children f3223bde5c87
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@267 11
adamc@267 12 <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 13
adamc@267 14 <p>The final part of the book applies the earlier parts' tools to examples in programming languages and compilers.</p>
adamc@267 15
adamc@267 16 <p>Interested in beta testing this book in a course you're teaching? Please <a href="">drop me a line</a>!</p>
adamc@39 17 </div>
adamc@39 18
adamc@39 19 <div class="project">
adamc@226 20 <h2>Distribution Formats</h2>
adamc@39 21 <ul>
adamc@39 22 <li> <a href="cpdt.pdf">Latest draft as a PDF</a></li>
adamc@39 23 <li> <a href="html/toc.html">Online version of latest draft, as hyperlinked HTML</a></li>
adamc@39 24 <li> <a href="cpdt.tgz">Tarball of Coq source to latest draft</a></li>
adamc@226 25 </ul>
adamc@226 26 </div>
adamc@226 27
adamc@226 28 <div class="project">
adamc@226 29 <h2>Used by:</h2>
adamc@226 30 <ul>
adamc@226 31 <li> CS252 at Harvard <a href="">(Fall 2008)</a></li>
adamc@226 32 </ul>
adamc@226 33 </div>
adamc@226 34
adamc@226 35 <div class="project">
adamc@226 36 <h2>Status</h2>
adamc@226 37
adamc@266 38 <p>Updated on November 16, 2009 with a version retargeted to Coq 8.2pl1. Last incremental update on December 30, 2009.</p>
adamc@231 39
adamc@266 40 <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 41
adamc@266 42 <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 43
adamc@267 44 <p>I'm also not sure how much of the final part, on programming languages and compilers, belongs in this book. It might change significantly or go away.</p>
adamc@39 45 </div>
adamc@39 46
adamc@39 47 </body></html>