| The materials here are superceded by the in-progress book Certified Programming with Dependent Types. |
Instructors: Adam Chlipala and George Necula.
When: Thursday 2:00-3:30
Where: Soda 310
To make projects easier, we are developing a Coq library containing common data structures and other useful tidbits.
Each group will have a 25-minute slot (including questions) to present its class project in one of the last two classes, which are Tuesday, December 5, and Thursday, December 7. Written project reports (which should be about 5 pages long) are due on the Monday after classes end, December 11. More details will follow.
| # | Date | Topics | Slides | Code | Homework out | Homework due |
|---|---|---|---|---|---|---|
| 1 | 8/29 | Introduction | OpenOffice | PDF | Andersen's analysis | HW0 | |
| 2 | 8/31 | Basic logic and natural deduction | OpenOffice | PDF | Sum example, natural deduction examples | HW1 [checker] (natural deduction reference) |
HW0 |
| 3 | 9/7 | Data structures and induction | OpenOffice | PDF | Peano arithmetic examples | HW2 [checker] | HW1 [solution] |
| 4 | 9/14 | Inductively-defined predicates | OpenOffice | PDF | lecture4 | HW3 | HW2 [solution] |
| 5 | 9/21 | Proofs as programs | PowerPoint | PDF | lect5 | HW4 | HW3 [solution] |
| 6 | 9/28 | Tactics for automation | OpenOffice | PDF | tsafe, lecture6 | HW5 | HW4 [solution] |
| 7 | 10/5 | Programming with proofs | OpenOffice | PDF | lecture7 | HW6 | HW5 [solution] |
| 8 | 10/12 | Easier programming with proofs | lecture8 | HW7 | HW6 [solution] | |
| 9 | 10/19 | Beyond primitive recursion | OpenOffice | PDF | lecture9, OCaml code | HW7 | |
| 10 | 10/26 | More fun with automation | lecture10 | |||
| 11 | 11/2 | Proof by reflection | OpenOffice | PDF | lecture11 (size comparison) | ||
| 12 | 11/9 | Denotational semantics | lecture12 | |||
| 13 | 11/16 | Reflecting Coq into Coq | lecture13 | |||
| 14 | 11/23 | Twelf | OpenOffice | PDF | nat, stlc | ||
| 15 | 12/5 | Project presentations I | ||||
| 16 | 12/7 | Project presentations II | ||||
| 12/11 | Project reports due by e-mail | |||||