Certified Programming with Dependent Types: staging/ex/index.html annotate

Builds with Coq 8.15.2

author	Adam Chlipala <adam@chlipala.net>
date	Sun, 31 Jul 2022 14:48:22 -0400
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>

Mercurial > cpdt > repo