lecture notes, handouts 
slides 
codeLecture topics, assignment due dates, and exam dates are subject to change.
Legend: lecture notes, handouts slides code
| DATE | EVENT | TOPIC | READINGS | LINKS |
|---|---|---|---|---|
| 1/22 | OCaml demo (in class) | |
||
| Operational Semantics and Proof Techniques | ||||
| 1/24 | Lecture 1 | Course Introduction | |
|
| 1/27 | Lecture 2 | The λ-Calculus | |
|
| 1/29 | Lecture 3 | λ-Calculus Encodings | |
|
| 1/31 | Lecture 4 | Reduction Strategies and Equivalence | |
|
| 2/3 | Lecture 5 | Recursion and Fixpoint Combinators | |
|
| 2/5 | Lecture 6 | Structural Operational Semantics and IMP | |
|
| 2/7 | Lecture 7 | Well-Founded Induction | |
|
| 2/10 | Assignment 1 due | |||
| 2/10 | Lecture 8 | Inductive Definitions and Least Fixpoints | |
|
| 2/12 | Lecture 9 | Evaluation Contexts | |
|
| Language Features | ||||
| 2/14 | Lecture 10 | Semantics via Translation | |
|
| 2/15–2/18 | February Break | |||
| 2/19 | Lecture 11 | A Functional Language | |
|
| 2/21 | Lecture 12 | Static vs Dynamic Scope | |
|
| 2/24 | Lecture 13 | Modules and State | |
|
| 2/26 | Lecture 14 | Continuations | |
|
| 2/28 | Assignment 2 due | |||
| 2/28 | Lecture 15 | Continuations and Exceptions | |
|
| Denotational Semantics | ||||
| 3/3 | Lecture 20 | Denotational Semantics | |
|
| 3/5 | Lecture 21 | CPOs and Continuous Functions | |
|
| 3/7 | Lecture 22 | Domain Constructions | |
|
| 3/10 | Lecture 23 | Denotational Semantics of REC | |
|
| 3/12 | Lecture 24 | Scott's D∞ Construction | |
|
| Axiomatic Semantics | ||||
| 3/14 | Lecture 16 | Predicate Transformers | |
|
| 3/17 | Lecture 17 | Hoare Logic | |
|
| 3/17 | Assignment 3 due | |||
| 3/17–3/28 | Prelim Exam | |||
| 3/19 | Lecture 18 | Dynamic Logic and Kleene Algebra | |
|
| 3/21 | Lecture 19 | Constructions in Dynamic Logic and Kleene Algebra | |
|
| Types | ||||
| 3/24 | Lecture 25 | Typed λ-Calculus | |
|
| 3/26 | Lecture 26 | Soundness of the Typing Rules | |
|
| 3/28 | Lecture 27 | Products, Sums, and Other Datatypes | |
|
| 3/29–4/6 | Spring Break | |||
| 4/7 | Lecture 28 | Strong Normalization | |
|
| 4/9 | Lecture 29 | Type Inference and Unification | |
|
| 4/11 | Lecture 30 | The Polymorphic λ-Calculus | |
|
| 4/14 | Lecture 31 | Propositions as Types | |
|
| 4/16 | Lecture 32 | Propositions as Types II | |
|
| 4/18 | Lecture 33 | Subtype Polymorphism | |
|
| 4/21 | Assignment 4 due | |||
| 4/21 | Lecture 34 | Recursive Types | |
|
| 4/23 | Lecture 35 | Testing Equirecursive Equality | |
|
| 4/25 | Lecture 36 | Coinductive Subtyping of Recursive Types | |
|
| 4/28 | Lecture 37 | Type Inference for Partial Types | |
|
| Topics | ||||
| 4/30 | Lecture 38 | Abstract Interpretation | |
|
| 5/2 | Lecture 40 | Existential Types | |
|
| 5/5 | Lecture 39 | Capsules | ||
| 5/7 | Assignment 5 due | |||
| 5/7 | Lecture 41 | Monads | |
|
| 5/8 | Slope Day | |||
| 5/7–5/16 | Final Exam | |||