|
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á <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ü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äskylä <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@570
|
101 <p><img src="scholar.jpg" width="205" height="207"><br></p>
|
|
adam@570
|
102 <p>One scholar appreciating the book</p>
|
|
adam@570
|
103
|
|
adam@553
|
104 <script src="//z-na.amazon-adsystem.com/widgets/onejs?MarketPlace=US&adInstanceId=14c7f9de-2f5e-4edd-af33-33d7e49e3296"></script>
|
|
adam@553
|
105
|
|
adamc@39
|
106 </body></html>
|
