-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathindex.html
1 lines (1 loc) · 2.28 KB
/
index.html
1
<html><head><title>The Little Prover</title><link rel="stylesheet" type="text/css" href="layout.css"/></head><body><div class="title_box"><table cellpadding="10px"><tr valign="top"><td><a href="https://mitpress.mit.edu/books/little-prover"><img src="book-cover.jpg"/></a></td><td><div><h1>The Little Prover</h1><p class="thin_para">Written by <a href="mailto:[email protected]">Daniel P. Friedman</a> and <a href="mailto:[email protected]">Carl Eastlund</a><br/>Drawings by Duane Bibby<br/>Foreword by <a href="https://www.cs.utexas.edu/users/moore/">J Strother Moore</a><br/>Afterword by <a href="http://www.ccs.neu.edu/home/matthias/">Matthias Felleisen</a></p><p class="thin_para"><a href="https://mitpress.mit.edu/books/little-prover">Available from MIT Press</a></p></div></td></tr></table></div><div class="title_box"><h1>J-Bob</h1><p class="wide_para">J-Bob is our little proof assistant, available on <a href="https://github.com/the-little-prover/j-bob">Github</a>. For an introduction to J-Bob, see Appendix A of The Little Prover.</p><p class="wide_para">J-Bob is available for <a href="http://www.cs.utexas.edu/users/moore/acl2/">ACL2</a>, <a href="http://www.schemers.org/">Scheme</a>, and <a href="http://racket-lang.org/">Racket</a> (via the <a href="http://dracula-lang.github.io/">Dracula</a> package). J-Bob is open source, feel free to adapt our proof assistant to the programming language of your choice. </p><p class="wide_para">Bear in mind that J-Bob is simple so that its source code can be read and understood. As a result, using J-Bob can be tedious and tricky at best. We sympathize with any difficulties you have, and we look forward to the creative extensions that users of J-Bob may come up with to make it easier. </p></div><div class="title_box"><h1>Errata</h1><p class="wide_para">Pages 165-166: replace all occurrences of "cheese" by "eggs"</p><p class="wide_para">Page 167: Frame 10 RHS: add "-31" to the right of "29"</p><p class="wide_para">Page 169: Frame 21 LHS: drop "of chapter 2"</p><p class="wide_para">Page 170: Frame 25 LHS: drop "of chapter 2"</p><p class="wide_para">Page 171: Frame 32 LHS: drop "of chapter 3"</p><p class="wide_para">Page 178: Frame 60 LHS: drop "of chapter 5"</p><p class="wide_para">Page 178: Frame 60 LHS: replace "56" by "55"</p></div><br/><br/></body></html>