Mercurial > cpdt > repo

comparison staging/index.html @ 366:03e200599633

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Remove home page reference to Part IV
author Adam Chlipala <adam@chlipala.net>
date Sun, 06 Nov 2011 16:54:40 -0500
parents 4a432659a698
children 31fa03bc0f18
comparison
equal deleted inserted replaced
365:990151eac6af 366:03e200599633
9 9
10 <div class="summary"> 10 <div class="summary">
11 <p>This is the web site for an in-progress textbook about practical engineering with <a href="http://coq.inria.fr/">the Coq proof assistant</a>. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation.</p> 11 <p>This is the web site for an in-progress textbook about practical engineering with <a href="http://coq.inria.fr/">the Coq proof assistant</a>. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation.</p>
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
15 <p>The final part of the book applies the earlier parts' tools to examples in programming languages and compilers.</p>
16 14
17 <p>Interested in beta testing this book in a course you're teaching? Please <a href="mailto:adamc@csail.mit.edu">drop me a line</a>!</p> 15 <p>Interested in beta testing this book in a course you're teaching? Please <a href="mailto:adamc@csail.mit.edu">drop me a line</a>!</p>
18 16
19 <p>A traditional hardcopy version will appear from <a href="http://mitpress.mit.edu/">MIT Press</a> Real Soon Now<a href="http://www.catb.org/jargon/html/R/Real-Soon-Now.html">*</a>.</p> 17 <p>A traditional hardcopy version will appear from <a href="http://mitpress.mit.edu/">MIT Press</a> Real Soon Now<a href="http://www.catb.org/jargon/html/R/Real-Soon-Now.html">*</a>.</p>
20 </div> 18 </div>