Mercurial > cpdt > repo

comparison staging/index.html @ 270:fd46d077b952

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Bug fixes
author Adam Chlipala <adamc@hcoop.net>
date Wed, 03 Feb 2010 08:17:02 -0500
parents f3223bde5c87
children e2dbc0f1c1e8
comparison
equal deleted inserted replaced
269:191a66cd7cb5 270:fd46d077b952
12 12
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> 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>
14 14
15 <p>The final part of the book applies the earlier parts' tools to examples in programming languages and compilers.</p> 15 <p>The final part of the book applies the earlier parts' tools to examples in programming languages and compilers.</p>
16 16
17 <p>Interested in beta testing this book in a course you're teaching? Please <a href="mailto:adamc@hcoop.net">drop me a line</a>!</p> 17 <p>Interested in beta testing this book in a course you're teaching? Please <a href="mailto:adam@chlipala.net">drop me a line</a>!</p>
18 </div> 18 </div>
19 19
20 <div class="project"> 20 <div class="project">
21 <h2>Distribution Formats</h2> 21 <h2>Distribution Formats</h2>
22 <ul> 22 <ul>
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 December 30, 2009.</p> 40 <p>Updated on November 16, 2009 with a version retargeted to Coq 8.2pl1. Last incremental update on February 3, 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