15-317 Constructive Logic
Schedule
- Lectures are Tuesday and Thursday in GHC 4102.
-
Recitations are Wednesday in WeH 4623.
Where a topic is not otherwise noted, recitations cover the material
from the preceding two lectures.
-
There may be occasional supplemental handouts on lecture material, but you are
expected to attend and take notes.
- The schedule is subject to change throughout the semester.
| Date |
Lecture or Recitation |
Homework Due |
|
| Tue | Aug | 24 |
Overview |
|
| Thu | Aug | 26 |
Natural Deduction |
|
|
| Tue | Aug | 31 |
Harmony |
|
| Thu | Sep | 2 |
Proofs as Programs |
|
|
| Tue | Sep | 7 |
β-reduction and Substitution |
|
| Thu | Sep | 9 |
Quantification and Natural Numbers |
Homework 1 |
|
| Tue | Sep | 14 |
Sequent Calculus |
|
| Thu | Sep | 16 |
Cut Elimination |
Homework 2 |
|
| Tue | Sep | 21 |
Cut Elimination |
|
| Thu | Sep | 23 |
Unprovability |
Homework 3 |
|
| Tue | Sep | 28 |
Classical Logic |
|
| Thu | Sep | 30 |
Midterm I |
Homework 4 |
|
| Tue | Oct | 5 |
Classical Logic |
|
| Thu | Oct | 7 |
Classical Computation/Inversion |
|
|
| Tue | Oct | 12 |
Theorem Proving: G4IP |
|
| Thu | Oct | 14 |
Theorem Proving: Inversion |
Homework 5 |
|
| Tue | Oct | 19 |
Logic Programming |
|
| Thu | Oct | 21 |
Theorem Proving, Redux |
Homework 6 |
|
| Tue | Oct | 26 |
Typed Prolog / Higher-Order Logic Programming |
|
| Thu | Oct | 28 |
Total Logic Programming |
Homework 7 |
|
| Tue | Nov | 2 |
Dependent Types |
|
| Thu | Nov | 4 |
Midterm II |
Homework 8 |
|
| Tue | Nov | 9 |
LF Type Theory |
|
| Thu | Nov | 11 |
Higher-Order Abstract Syntax |
|
|
| Tue | Nov | 16 |
Higher-Order Judgments |
|
| Thu | Nov | 18 |
Logic Programming in Elf |
Homework 9 |
|
| Tue | Nov | 23 |
Twelf |
|
| Thu | Nov | 25 |
Thanksgiving Break (no classes) |
|
|
| Tue | Nov | 30 |
Linear Logic |
|
| Thu | Dec | 2 |
Linear Logic |
Homework 10 |
[ Home
| Schedule
| Assignments
| Software
]
|