Date | Lecture | Homework | ||||
---|---|---|---|---|---|---|
|
||||||
We | Sep | 5 | Overview/Natural Deduction | |||
Fr | Sep | 7 | Natural Deduction | |||
|
||||||
Mo | Sep | 10 | Tutorial (Maja) |   | ||
We | Sep | 12 | Tutorial (Maja) | |||
Fr | Sep | 14 | Normal Proofs | HW 1 out / | ||
|
||||||
Mo | Sep | 17 | Notational definitions | |||
We | Sep | 19 | Proofs-as-Programs (1) | |||
Fr | Sep | 21 | Proofs-as-Programs | HW 1 due / HW 2 out | ||
|
||||||
Mo | Sep | 24 | Properties of proof terms | |||
We | Sep | 26 | Lambda-calculus | |||
Fr | Sep | 28 | Primitive recursion | HW 2 due / HW 3 out | ||
|
||||||
Mo | Oct | 1 | Data-types | |||
We | Oct | 3 | Induction | |||
Fr | Oct | 5 | to be announced | HW 3 due / HW 4 out | ||
|
||||||
Mo | Oct | 8 | Thanksgiving Holiday | |||
Tu | Oct | 9 | First-order logic | |||
We | Oct | 10 | First-order logic | |||
Fr | Oct | 12 | First-order logic | HW 4 due / HW 5 out | ||
|
||||||
Mo | Oct | 15 | Contracting proofs | |||
We | Oct | 17 | Reasoning about data | |||
Fr | Oct | 19 | Review | HW 5 due | ||
|
||||||
Mo | Oct | 22 | Midterm | |||
We | Oct | 24 | Normal natural deduction | |||
Fr | Oct | 26 | Consistency | |||
|
||||||
Mo | Oct | 29 | Sequent Calculus | |||
We | Oct | 31 | Meta-theoretic properties | |||
Fr | Nov | 2 | Inversion and focusing | Project Proposal due | ||
|
||||||
Mo | Nov | 5 | Guided theorem prover | |||
We | Nov | 7 | Logic Programming | |||
Fr | Nov | 9 | Logic Programming | |||
|
||||||
Mo | Nov | 12 | Forward theorem proving | |||
We | Nov | 14 | Forward theorem proving | |||
Fr | Nov | 16 | Bi-directional theorem proving | Project Milestone | ||
|
||||||
Mo | Nov | 19 | Special topic: Modal logic | |||
We | Nov | 21 | Special topic: Dependent types | |||
Fr | Nov | 23 | Special topic: Linear logic | |||
|
||||||
Mo | Nov | 26 | Presentations | |||
We | Nov | 28 | Presentations | |||
Fr | Nov | 30 | Presentations | |||
|
||||||
Mo | Dec | 3 | Presentations | |||
|