annotate staging/ex/index.html @ 569:0ce9829efa3b
Back to working in Coq 8.4
| author |
Adam Chlipala <adam@chlipala.net> |
| date |
Sun, 20 Jan 2019 15:28:23 -0500 |
| parents |
c8a3cb24bae9 |
| children |
|
| rev |
line source |
|
adam@489
|
1 <html>
|
|
adam@489
|
2 <head>
|
|
adam@489
|
3 <link rel="stylesheet" type="text/css" href="/style.css">
|
|
adam@489
|
4 <title>Certified Programming with Dependent Types Exercises</title>
|
|
adam@489
|
5 </head><body>
|
|
adam@489
|
6 <h1><a href="..">Certified Programming with Dependent Types</a> Exercises</h1>
|
|
adam@489
|
7
|
|
adam@489
|
8 <div class="summary">
|
|
adam@489
|
9 <p>Here lies an attempt to crowdsource the production of exercises for CPDT.</p>
|
|
adam@489
|
10 </div>
|
|
adam@489
|
11
|
|
adam@489
|
12 <div class="project">
|
|
adam@490
|
13 <h2>Exercises Written for CPDT</h2>
|
|
adam@489
|
14 <ul>
|
|
adam@489
|
15 <li> <a href="exercises.pdf">Snapshot of exercises that were included in CPDT when I decided to stop maintaining exercises</a> (<a href="http://adam.chlipala.net/">Adam Chlipala</a>)</li>
|
|
adam@489
|
16 <li> <a href="http://www.cis.upenn.edu/~bcpierce/courses/670Fall12/">Homeworks from CIS 670 at Penn in Fall 2012</a> (<a href="http://www.cis.upenn.edu/~bcpierce/">Benjamin Pierce</a> and students in the class)</li>
|
|
adam@489
|
17 </ul>
|
|
adam@489
|
18 </div>
|
|
adam@489
|
19
|
|
adam@490
|
20 <div class="project">
|
|
adam@490
|
21 <h2>Other Exercises</h2>
|
|
adam@490
|
22 <ul>
|
|
adam@490
|
23 <li> <a href="http://www.labri.fr/perso/casteran/CoqArt/contents.html">Coq'Art exercises</a> (<a href="http://www-sop.inria.fr/lemme/Yves.Bertot/index.html">Yves Bertot</a> and <a href="http://www.labri.fr/Perso/~casteran/index.html">Pierre Castéran</a>)</li>
|
|
adam@490
|
24 </ul>
|
|
adam@490
|
25 </div>
|
|
adam@490
|
26
|
|
adam@489
|
27 </body></html>
|
