<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>
<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>
<p>The final part of the book applies the earlier parts' tools to examples in programming languages and compilers.</p>
<p>Interested in beta testing this book in a course you're teaching? Please <ahref="mailto:adamc@csail.mit.edu">drop me a line</a>!</p>
<p>Interested in beta testing this book in a course you're teaching? Please <ahref="mailto:adamc@csail.mit.edu">drop me a line</a>!</p>
<p>A traditional hardcopy version will appear from <ahref="http://mitpress.mit.edu/">MIT Press</a> Real Soon Now<ahref="http://www.catb.org/jargon/html/R/Real-Soon-Now.html">*</a>.</p>
<p>A traditional hardcopy version will appear from <ahref="http://mitpress.mit.edu/">MIT Press</a> Real Soon Now<ahref="http://www.catb.org/jargon/html/R/Real-Soon-Now.html">*</a>.</p>
