Note: this page formerly held solutions to the exercises. If you would like a copy of the solutions, please email Benjamin.
Note: this schedule is very tentative!
| Week | Monday | Wednesday | Friday |
|---|---|---|---|
| Sep 3-7 | Lecture 1: Introduction,
functional programming (numbers, lists)
Slides, Coq script |
First recitation | |
| Sep 10-14 | Lecture 2: Functional programming (higher-order functions, polymorphism) HW01 due (basic functional programming); instructions |
Lecture 3: induction; proofs about numbers and lists | |
| Sep 17-21 | Lecture 4: More Coq tactics HW02 due (more functional programming; basic induction) |
Lecture 5: Simple interpreters | |
| Sep 24-28 | Lecture 6: More on induction;
programming with propositions HW03 due (simple interpreters) |
Lecture 7: Inductive definitions of logical connectives | |
| Oct 1-5 | Lecture 8: Induction principles, relations, operational semantics HW04 due (programming with propositions, logical connectives) |
Lecture 9: Operational semantics | |
| Oct 8-12 |
Lecture 10: Review HW05 due (Operational semantics) |
Midterm I (review questions, review questions with solutions, exam, exam with solutions) | |
| Oct 15-19 | Fall break (no class Oct 15th) | Lecture 11: More operational semantics; basic automation | |
| Oct 22-26 | Lecture 12: Types HW06 due (Operational semantics; automation) |
Lecture 13: Untyped lambda-calculus (TAPL chapter 5) | |
| Oct 29-Nov 2 | Lecture 14: Programming in the lambda-calculus HW07 due (operational semantics; untyped lambda-calculus) |
Lecture 15: Properties of evaluation | |
| Nov 5-9 | Lecture 16: Behavioral equivalence HW08 due (untyped lambda-calculus) |
Lecture 17: Simple types (TAPL chapters 8 and 9) | |
| Nov 12-16 | Review
HW09 due (behavioral equivalence, simple types) |
Midterm II (review questions, review questions with solutions, exam, exam with solutions) | |
| Nov 19-23 | Lecture 18: Extensions of simple types (TAPL chapter 11) | Lecture 19: Extensions of simple types | Thanksgiving break (no recitation) |
| Nov 26-29 | Lecture 20: Subtyping (TAPL
chapter 15 and part of 16) HW10 due (extensions of simple types) |
Lecture 21: Subtyping | |
| Dec 3-7 | Lecture 22: Algorithmic subtyping
and typing (course evaluations) HW11 due (subtyping) |
Lecture 23: Featherweight Java (supplemental slides | Dec 7: Last day of classes |
| Dec 10-14 | Reading days (through Dec 11), final exams week
HW12 due Dec 10 (FJ) |
||
| Dec 17-21 | FINAL EXAM: Tuesday, Dec 18, 12-2, Moore 216
(review questions, review questions with solutions, exam with solutions) |
||