Mercurial > cpdt > repo

<html>
<head>
<link rel="alternate" type="application/rss+xml" title="Updates RSS Feed" href="updates.rss">
<link rel="stylesheet" type="text/css" href="/style.css">
<title>Certified Programming with Dependent Types</title>
</head><body>
<h1>Certified Programming with Dependent Types</h1>
<h2><a href="http://adam.chlipala.net/">Adam Chlipala</a></h2>

<div class="summary" style="overflow: hidden">
<img src="cover.jpg" width="300" height="390" align="left" style="margin-right: 30px" alt="book cover">

<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>

<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>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>

<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>

<h2>Buy a Copy in Print</h2>
<ul>
<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/>
<a href="http://mitpress.mit.edu/books/certified-programming-dependent-types">The MIT Press page for the book</a><br/>
<b>ISBN:</b> 9780262026659
</ul>
</div>

<div class="project">
<h2>Distribution Formats (free version)</h2>
<ul>
<li> <a href="cpdt.pdf">Latest draft as a PDF</a></li>
<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>
<li> <a href="cpdt.tgz">Tarball of Coq source to latest draft</a></li>
<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>
<li> <a href="repo">Public, read-only Mercurial repository</a></li>
<li> <a href="updates.rss">RSS feed of updates</a></li>
</ul>
</div>

<div class="project">
<h2><a href="ex/">Online Collection of Exercises for the Book</a></h2>
</div>

<div class="project">
<h2>Use in classes</h2>

<h3>Classes where CPDT is/was the primary text</h3>
<ul>
<li>CS691PL at U. Mass. Amherst <a href="https://www.cs.umass.edu/~arjun/courses/cs691pl-spring2014/">(Spring 2014)</a></li>
<li>CSE 506 at U. Washington <a href="http://courses.cs.washington.edu/courses/cse506/14wi/">(Winter 2014)</a></li>
<li>EECS 395 at Northwestern <a href="http://www.eecs.northwestern.edu/~robby/courses/395-495-2013-fall/">(Fall 2013)</a></li>
<li>CIS 670 at Penn <a href="http://www.cis.upenn.edu/~bcpierce/courses/670Fall12/">(Fall 2012)</a></li>
<li>6.892 at MIT <a href="http://stellar.mit.edu/S/course/6/fa11/6.892/">(Fall 2011)</a></li>
<li>CS252 at Harvard <a href="http://www.cs.harvard.edu/~adamc/cpdt/">(Fall 2008)</a></li>
</ul>

<h3>Classes where CPDT is/was a supplementary text</h3>
<ul>
<li>CS 565 at Purdue <a href="https://www.cs.purdue.edu/homes/gpetri/cs565-spring2014/">(Spring 2014)</a></li>
<li>CMPS203 at UC Santa Cruz <a href="http://courses.soe.ucsc.edu/courses/cmps203/Winter14/01">(Winter 2014)</a></li>
<li>CS 430 at Yale <a href="http://flint.cs.yale.edu/cs430/info.html">(Fall 2013)</a></li>
<li>CS410 at Portland State <a href="http://web.cecs.pdx.edu/~apt/cs510coq/">(Spring 2013)</a></li>
<li>IFT 6172 at U. Montreal <a href="http://www.iro.umontreal.ca/~monnier/6172/">(Spring 2013)</a></li>
<li>TIES341 at U. Jyv&auml;skyl&auml; <a href="http://functional-programming.it.jyu.fi/TIES343/TIES341.html">(Spring 2013)</a></li>
<li>CS252r at Harvard <a href="http://www.eecs.harvard.edu/~greg/cs252rfa11/">(Fall 2011)</a></li>
<li>G54DTP at Nottingham <a href="http://www.cs.nott.ac.uk/~vxc/g54dtp/g54dtp.html">(Spring 2011)</a></li>
</ul>

<h3>Reading groups</h3>
<ul>
<li>CS 7190 at Cornell <a href="http://www.cs.cornell.edu/projects/pldg/archives.php">(Summer 2013)</a></li>
<li>At U. Wisconsin <a href="http://pages.cs.wisc.edu/~mulhern/coqtalks/2008.09/">(2008-2009)</a></li>
</ul>
</div>

<div class="project">
<h2>Old versions</h2>

<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>
</div>

</body></html>
author	Adam Chlipala <adam@chlipala.net>
date	Sun, 23 Mar 2014 16:20:08 -0400
parents	ff7951e3134a
children	66c35ffcab4e