Mercurial > cpdt > repo

annotate staging/index.html @ 567:ec0ce5129fc4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Switch to new approach to supporting newer Coq versions while still building with patched Coq 8.4
author Adam Chlipala <adam@chlipala.net>
date Sun, 20 Jan 2019 15:00:32 -0500
parents 1a231194d164
children c3d4217e1da7
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="http://adam.chlipala.net/">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="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>
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="mailto:adamc@csail.mit.edu">drop me a line</a>!</p>
adam@299 18
adam@518 19 <p>A traditional hardcopy version is available from <a href="http://mitpress.mit.edu/">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="http://www.amazon.com/gp/product/0262026651/ref=as_li_tf_tl?ie=UTF8&camp=1789&creative=9325&creativeASIN=0262026651&linkCode=as2&tag=adamchli-20">From Amazon.com</a><img src="http://ir-na.amazon-adsystem.com/e/ir?t=adamchli-20&l=as2&o=1&a=0262026651" width="1" height="1" border="0" alt="" style="border:none !important; margin:0px !important;" /><br/>
adam@521 24 <a href="http://mitpress.mit.edu/books/certified-programming-dependent-types">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@557 48 <h3>Classes where CPDT is/was a primary text</h3>
adamc@226 49 <ul>
adam@560 50 <li>CK0230 at Universidade Federal do Cear&aacute; <a href="http://lia.ufc.br/~pmsf/2017-2/pac/">(Fall 2017)</a></li>
adam@555 51 <li>EECS 755 at U. Kansas <a href="http://perry.alexander.name/eecs755/">(Fall 2017)</a></li>
adam@525 52 <li>CS691PL at U. Mass. Amherst <a href="https://www.cs.umass.edu/~arjun/courses/cs691pl-spring2014/">(Spring 2014)</a></li>
adam@522 53 <li>CSE 506 at U. Washington <a href="http://courses.cs.washington.edu/courses/cse506/14wi/">(Winter 2014)</a></li>
adam@516 54 <li>EECS 395 at Northwestern <a href="http://www.eecs.northwestern.edu/~robby/courses/395-495-2013-fall/">(Fall 2013)</a></li>
adam@481 55 <li>CIS 670 at Penn <a href="http://www.cis.upenn.edu/~bcpierce/courses/670Fall12/">(Fall 2012)</a></li>
adam@308 56 <li>6.892 at MIT <a href="http://stellar.mit.edu/S/course/6/fa11/6.892/">(Fall 2011)</a></li>
adam@308 57 <li>CS252 at Harvard <a href="http://www.cs.harvard.edu/~adamc/cpdt/">(Fall 2008)</a></li>
adamc@226 58 </ul>
adam@526 59
adam@526 60 <h3>Classes where CPDT is/was a supplementary text</h3>
adam@526 61 <ul>
adam@566 62 <li>ITP at U. T&uuml;bingen <a href="http://ps.informatik.uni-tuebingen.de/teaching/ws18/itp/">(Winter 2018/2019)</a></li>
adam@566 63 <li>CS410 at Portland State (<a href="http://web.cecs.pdx.edu/~apt/cs510coq/">Fall 2018</a>, Spring 2013)</li>
adam@565 64 <li>CSI 5137 at U. Ottawa (<a href="http://www.site.uottawa.ca/~afelty/csi5137/">Fall 2018</a>)</li>
adam@562 65 <li>6.822 at MIT (<a href="https://frap.csail.mit.edu/">Spring 2018</a>, Spring 2017, Spring 2016)</li>
adam@558 66 <li>CS 6115 at Cornell <a href="http://www.cs.cornell.edu/courses/cs6115/2017fa/">(Fall 2017)</a></li>
adam@560 67 <li>CS750 at IIT Kanpur <a href="https://www.cse.iitk.ac.in/users/ppk/teaching/Programs-Proofs-and-Types/">(Fall 2017)</a></li>
adam@561 68 <li>6.820 at MIT (<a href="https://learning-modules.mit.edu/class/index.html?uuid=/course/6/fa17/6.820">Fall 2017</a>, <a href="http://stellar.mit.edu/S/course/6/fa15/6.820/">Fall 2015</a>, <a href="http://stellar.mit.edu/S/course/6/fa13/6.820/">Fall 2013</a>)</li>
adam@564 69 <li>CSCI 740 at RIT <a href="https://cs.rit.edu/~hh/teaching/plt17/">(Fall 2017)</a></li>
adam@556 70 <li>CMSC631 at U. Maryland <a href="http://cs.umd.edu/class/fall2017/cmsc631/">(Fall 2017)</a></li>
adam@559 71 <li>CS260r at Harvard <a href="http://read.seas.harvard.edu/~kohler/class/cs260r-17/">(Spring 2017)</a></li>
adam@531 72 <li>CS250 at Harvard <a href="http://www.eecs.harvard.edu/~greg/cs250fall2014/">(Fall 2014)</a></li>
adam@526 73 <li>CS 565 at Purdue <a href="https://www.cs.purdue.edu/homes/gpetri/cs565-spring2014/">(Spring 2014)</a></li>
adam@530 74 <li>Formal Methods at UST China <a href="http://staff.ustc.edu.cn/~bjhua/courses/theory/2014/index.html">(Spring 2014)</a></li>
adam@529 75 <li>185.A60 at TU Vienna <a href="https://tiss.tuwien.ac.at/course/courseDetails.xhtml?windowId=ddd&courseNr=185A60&semester=2014S">(Spring 2014)</a></li>
adam@526 76 <li>CMPS203 at UC Santa Cruz <a href="http://courses.soe.ucsc.edu/courses/cmps203/Winter14/01">(Winter 2014)</a></li>
adam@526 77 <li>CS 430 at Yale <a href="http://flint.cs.yale.edu/cs430/info.html">(Fall 2013)</a></li>
adam@526 78 <li>IFT 6172 at U. Montreal <a href="http://www.iro.umontreal.ca/~monnier/6172/">(Spring 2013)</a></li>
adam@526 79 <li>TIES341 at U. Jyv&auml;skyl&auml; <a href="http://functional-programming.it.jyu.fi/TIES343/TIES341.html">(Spring 2013)</a></li>
adam@528 80 <li>CMPT 340 at U. Saskatchewan (Spring 2012)</li>
adam@526 81 <li>CS252r at Harvard <a href="http://www.eecs.harvard.edu/~greg/cs252rfa11/">(Fall 2011)</a></li>
adam@526 82 <li>G54DTP at Nottingham <a href="http://www.cs.nott.ac.uk/~vxc/g54dtp/g54dtp.html">(Spring 2011)</a></li>
adam@530 83 <li>Formal Methods at U. Zagreb <a href="http://titan.fsb.hr/~nslani/fm/Site/B424FC03-5F6D-4CD9-8A53-CB71DD137F42.html">(Spring 2011)</a></li>
adam@528 84 <li>CMPT 863 at U. Saskatchewan (Spring 2010)</li>
adam@526 85 </ul>
adam@526 86
adam@526 87 <h3>Reading groups</h3>
adam@526 88 <ul>
adam@526 89 <li>CS 7190 at Cornell <a href="http://www.cs.cornell.edu/projects/pldg/archives.php">(Summer 2013)</a></li>
adam@561 90 <li>At Radboud University Nijmegen (<a href="http://www.cs.ru.nl/~spitters/cpdt.html">2010</a>, <a href="http://cs.ru.nl/~dfrumin/cpdt.html">2016/2017</a>)</li>
adam@526 91 <li>At U. Wisconsin <a href="http://pages.cs.wisc.edu/~mulhern/coqtalks/2008.09/">(2008-2009)</a></li>
adam@526 92 </ul>
adamc@226 93 </div>
adamc@226 94
adamc@226 95 <div class="project">
adam@518 96 <h2>Old versions</h2>
adamc@267 97
adam@332 98 <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 99 </div>
adamc@39 100
adam@553 101 <script src="//z-na.amazon-adsystem.com/widgets/onejs?MarketPlace=US&adInstanceId=14c7f9de-2f5e-4edd-af33-33d7e49e3296"></script>
adam@553 102
adamc@39 103 </body></html>