| Date |
Lecture |
|
|
Homework |
|
| Tue | Jan | 6 |
Overview/Natural Deduction |
|
|
|
| Thu | Jan | 8 |
Natural Deduction |
|
|
|
|
| Tue | Jan | 13 |
Tutch tutorial |
|
|
|
| Thu | Jan | 15 |
Local soundness and completeness |
|
|
HW1 out |
|
| Tue | Jan | 20 |
Proofs as programs |
|
|
|
| Thu | Jan | 22 |
Subject reduction |
|
|
HW 1 due / HW 2 out |
|
| Tue | Jan | 27 |
Quantifiers |
|
|
|
| Thu | Jan | 29 |
Computational meaning |
|
|
HW 2 due / HW 3 out |
|
| Tue | Feb | 3 |
Classical Logic |
|
|
|
| Thu | Feb | 5 |
Proof irrelevance |
|
|
HW 3 due |
|
| Tue | Feb | 10 |
Review |
|
|
|
| Thu | Feb | 12 |
Midterm I |
|
|
|
|
| Tue | Feb | 17 |
Reasoning with data types |
|
|
HW 4 out |
| Thu | Feb | 19 |
Induction |
|
|
|
|
| Tue | Feb | 24 |
BREAK |
|
|
|
| Thu | Feb | 26 |
BREAK |
|
|
|
|
| Tue | Mar | 3 |
Logic programming |
|
|
|
| Thu | Mar | 5 |
Logic programming |
|
|
HW 4 due / HW 5 out |
|
| Tue | Mar | 10 |
Sequent Calculus |
|
|
|
| Thu | Mar | 12 |
Meta-theoretic properties |
|
|
HW 5 due / HW 6 out |
|
| Tue | Mar | 17 |
Inversion and Focusing |
|
|
|
| Thu | Mar | 19 |
Computations and focusing |
|
|
HW 6 due |
|
| Tue | Mar | 24 |
Review |
|
|
|
| Thu | Mar | 26 |
Midterm II |
|
|
Project proposal due |
|
| Tue | Mar | 31 |
Bottom-up logic programming |
|
|
|
| Thu | Apr | 2 |
Higher-order logic programming |
|
|
Milestone I due |
|
| Tue | Apr | 7 |
Presentations |
|
|
|
| Thu | Apr | 9 |
Presentations |
|
|
Milestone II due |
|