Mercurial > cpdt > repo

comparison staging/index.html @ 380:31fa03bc0f18

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Get it to build with Coq 8.4
author Adam Chlipala <adam@chlipala.net>
date Thu, 29 Mar 2012 18:10:52 -0400
parents 03e200599633
children c4a22c9ff090
comparison
equal deleted inserted replaced
379:e23d41ae63be 380:31fa03bc0f18
37 </div> 37 </div>
38 38
39 <div class="project"> 39 <div class="project">
40 <h2>Status</h2> 40 <h2>Status</h2>
41 41
42 <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="http://stellar.mit.edu/S/course/6/fa11/6.892/">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> 42 <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="http://stellar.mit.edu/S/course/6/fa11/6.892/">my fall class</a> and publication by MIT Press. I'm adding bibliographic references and index entries, along with the usual tweaks and improvements.</p>
43 43
44 <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> 44 <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>
45 45
46 <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> 46 <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>
47 47
48 <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> 48 <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>
49 </div> 49 </div>
50 50
51 </body></html> 51 </body></html>