Mercurial > cpdt > repo
comparison staging/index.html @ 293:e2dbc0f1c1e8
New release
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Wed, 10 Nov 2010 16:34:46 -0500 |
| parents | fd46d077b952 |
| children | 20c742997dae |
comparison
equal
deleted
inserted
replaced
| 292:2c88fc1dbe33 | 293:e2dbc0f1c1e8 |
|---|---|
| 35 </div> | 35 </div> |
| 36 | 36 |
| 37 <div class="project"> | 37 <div class="project"> |
| 38 <h2>Status</h2> | 38 <h2>Status</h2> |
| 39 | 39 |
| 40 <p>Updated on November 16, 2009 with a version retargeted to Coq 8.2pl1. Last incremental update on February 3, 2010.</p> | 40 <p>Updated on November 16, 2009 with a version retargeted to Coq 8.2pl1. Last incremental update on November 10, 2010.</p> |
| 41 | 41 |
| 42 <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> | 42 <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> |
| 43 | 43 |
| 44 <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> | 44 <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> |
| 45 | 45 |