The materials here are superceded by the in-progress book Certified Programming with Dependent Types.

Interactive Computer Theorem Proving

(CS294-9 Fall 2006)

Instructors: Adam Chlipala and George Necula.

When: Thursday 2:00-3:30

Where: Soda 310

Code Library

To make projects easier, we are developing a Coq library containing common data structures and other useful tidbits.

Project Information

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.


Administrivia page


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