| Date | Topics | Chapters | Handouts | |
|---|---|---|---|---|
| Jan | 16 | (No Class) | ||
| 18 | (No Class) | |||
| 23 | Introduction; What is Constructive Logic? | CL Ch. 1 | Meaning of the Logical Constants | |
| 25 | Judgements and Evidence; Conjunction and Truth; Hypotheses and Implication | CL Ch. 2 | Truth of a Proposition | |
| 30 | Hypothetical Judgements; Disjunction, Falsity, and Negation | Constructive Negation, Excluded Middle. | ||
| Feb | 1 | Normal Deductions and Non-Provability | Normal Deductions | |
| 6 | Completeness of Normal Deductions; Proofs as Programs | |||
| 8 | Proofs as Programs | CL Ch. 3 | Analytic and Synthetic Judgments | |
| 13 | Proofs as Programs | |||
| 15 | Subject Reduction | Substitution, Proof Equivalence | ||
| 20 | Normalization | |||
| 22 | Normalization: Cut lemma | |||
| 27 | Types; Primitive Recursion | CL Ch. 4 | General Judgments | |
| Mar | 1 | Predicate logic; Quantifiers | ||
| 6 | Midterm Review; Normal Proofs and Quantifiers | |||
| 8 | Midterm Exam | |||
| 13 | (Spring Break) | |||
| 15 | (Spring Break) | |||
| 20 | Predicate Logic and Natural Numbers | CL Ch. 4 | ||
| 22 | Complete Induction; Program Extraction | Complete Induction | ||
| 27 | Classical Logic | Classical Logic | ||
| 29 | Classical Logic | |||
| Apr | 3 | Linear Logic | LL Chs 1, 2 | |
| 5 | Linear Logic and Regular Expression Matching | Matching as Deduction | ||
| 10 | LF | |||
| 12 | LF | |||
| 17 | LF | |||
| 19 | (Spring Carnival) | |||
| May | 1 | LF | ||
| 3 | LF | |||