annotate staging/index.html @ 531:977b425331c3

Link to Harvard CS250, Fall 2014
author Adam Chlipala <>
date Thu, 04 Sep 2014 07:22:03 -0400
parents 1dd9d8664853
children cb81f74d8c92
rev   line source
adamc@39 1 <html>
adamc@39 2 <head>
adamc@268 3 <link rel="alternate" type="application/rss+xml" title="Updates RSS Feed" href="updates.rss">
adamc@39 4 <link rel="stylesheet" type="text/css" href="/style.css">
adamc@39 5 <title>Certified Programming with Dependent Types</title>
adamc@39 6 </head><body>
adamc@39 7 <h1>Certified Programming with Dependent Types</h1>
adamc@69 8 <h2><a href="">Adam Chlipala</a></h2>
adamc@39 9
adam@518 10 <div class="summary" style="overflow: hidden">
adam@518 11 <img src="cover.jpg" width="300" height="390" align="left" style="margin-right: 30px" alt="book cover">
adam@518 12
adam@518 13 <p>This is the web site for a textbook about practical engineering with <a href="">the Coq proof assistant</a>. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation.</p>
adamc@267 14
adamc@267 15 <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>
adamc@267 16
adam@518 17 <p>Interested in using this book in a course you're teaching? Please <a href="">drop me a line</a>!</p>
adam@299 18
adam@518 19 <p>A traditional hardcopy version is available from <a href="">MIT Press</a>, who have graciously agreed to allow distribution of free versions online indefinitely, minus the benefits of the Press' copy editing!</p>
adam@518 20
adam@518 21 <h2>Buy a Copy in Print</h2>
adam@518 22 <ul>
adam@518 23 <a href="">From</a><img src="" width="1" height="1" border="0" alt="" style="border:none !important; margin:0px !important;" /><br/>
adam@521 24 <a href="">The MIT Press page for the book</a><br/>
adam@521 25 <b>ISBN:</b> 9780262026659
adam@518 26 </ul>
adamc@39 27 </div>
adamc@39 28
adamc@39 29 <div class="project">
adam@518 30 <h2>Distribution Formats (free version)</h2>
adamc@39 31 <ul>
adamc@39 32 <li> <a href="cpdt.pdf">Latest draft as a PDF</a></li>
adam@515 33 <li> <a href="html/toc.html">Online version of latest draft, as hyperlinked HTML</a> [note that the author focuses on the PDF version and doesn't make an effort to keep the HTML version particularly pleasant to use]</li>
adamc@39 34 <li> <a href="cpdt.tgz">Tarball of Coq source to latest draft</a></li>
adam@517 35 <li> <a href="cpdtlib.tgz">Tarball of a few generally useful library modules from the book</a> (which are released under an open-source license, while the book generally isn't)</li>
adam@321 36 <li> <a href="repo">Public, read-only Mercurial repository</a></li>
adamc@268 37 <li> <a href="updates.rss">RSS feed of updates</a></li>
adamc@226 38 </ul>
adamc@226 39 </div>
adamc@226 40
adamc@226 41 <div class="project">
adam@489 42 <h2><a href="ex/">Online Collection of Exercises for the Book</a></h2>
adam@489 43 </div>
adam@489 44
adam@489 45 <div class="project">
adam@526 46 <h2>Use in classes</h2>
adam@526 47
adam@526 48 <h3>Classes where CPDT is/was the primary text</h3>
adamc@226 49 <ul>
adam@525 50 <li>CS691PL at U. Mass. Amherst <a href="">(Spring 2014)</a></li>
adam@522 51 <li>CSE 506 at U. Washington <a href="">(Winter 2014)</a></li>
adam@516 52 <li>EECS 395 at Northwestern <a href="">(Fall 2013)</a></li>
adam@481 53 <li>CIS 670 at Penn <a href="">(Fall 2012)</a></li>
adam@308 54 <li>6.892 at MIT <a href="">(Fall 2011)</a></li>
adam@308 55 <li>CS252 at Harvard <a href="">(Fall 2008)</a></li>
adamc@226 56 </ul>
adam@526 57
adam@526 58 <h3>Classes where CPDT is/was a supplementary text</h3>
adam@526 59 <ul>
adam@531 60 <li>CS250 at Harvard <a href="">(Fall 2014)</a></li>
adam@526 61 <li>CS 565 at Purdue <a href="">(Spring 2014)</a></li>
adam@530 62 <li>Formal Methods at UST China <a href="">(Spring 2014)</a></li>
adam@529 63 <li>185.A60 at TU Vienna <a href="">(Spring 2014)</a></li>
adam@526 64 <li>CMPS203 at UC Santa Cruz <a href="">(Winter 2014)</a></li>
adam@526 65 <li>CS 430 at Yale <a href="">(Fall 2013)</a></li>
adam@526 66 <li>CS410 at Portland State <a href="">(Spring 2013)</a></li>
adam@526 67 <li>IFT 6172 at U. Montreal <a href="">(Spring 2013)</a></li>
adam@526 68 <li>TIES341 at U. Jyv&auml;skyl&auml; <a href="">(Spring 2013)</a></li>
adam@528 69 <li>CMPT 340 at U. Saskatchewan (Spring 2012)</li>
adam@526 70 <li>CS252r at Harvard <a href="">(Fall 2011)</a></li>
adam@526 71 <li>G54DTP at Nottingham <a href="">(Spring 2011)</a></li>
adam@530 72 <li>Formal Methods at U. Zagreb <a href="">(Spring 2011)</a></li>
adam@528 73 <li>CMPT 863 at U. Saskatchewan (Spring 2010)</li>
adam@526 74 </ul>
adam@526 75
adam@526 76 <h3>Reading groups</h3>
adam@526 77 <ul>
adam@526 78 <li>CS 7190 at Cornell <a href="">(Summer 2013)</a></li>
adam@527 79 <li>At Radboud University Nijmegen <a href="">(2010)</a></li>
adam@526 80 <li>At U. Wisconsin <a href="">(2008-2009)</a></li>
adam@526 81 </ul>
adamc@226 82 </div>
adamc@226 83
adamc@226 84 <div class="project">
adam@518 85 <h2>Old versions</h2>
adamc@267 86
adam@332 87 <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>
adamc@39 88 </div>
adamc@39 89
adamc@39 90 </body></html>