Skip to main content





Schedule

Lecture topics and assignment due dates are subject to change.

DATE EVENT TOPIC READINGS LINKS
Operational Semantics and Proof Techniques
1/25 Lecture 1 Course Introduction [Notes]
1/25 Assignment 1 issued [A1]
1/27 Lecture 2 The λ-Calculus [Notes][Handout]
1/28 OCaml demo, 7:30–9pm, Upson B7 Lab [fv.ml]
1/29 Lecture 3 λ-Calculus Encodings [Notes]
2/1 Lecture 4 Reduction Strategies and Equivalence [Notes]
2/3 Lecture 5 Recursion and Fixpoint Combinators [Notes]
2/5 Lecture 6 Structural Operational Semantics and IMP [Notes]
2/8 Lecture 7 Well-Founded Induction [Notes]
2/10 Assignment 1 due, Assignment 2 issued [A1] [A2]
2/10 Lecture 8 Inductive Definitions and Least Fixpoints [Notes][Handout]
2/12 Lecture 9 Evaluation Contexts [Notes]
Language Features
2/15 Lecture 10 Semantics via Translation [Notes]
2/17 Lecture 11 A Functional Language [Notes]
2/19 Lecture 12 Static vs Dynamic Scope [Notes]
2/22 Lecture 13 Modules and State [Notes][Handout]
2/24 Lecture 14 Continuations [Notes]
2/26 Assignment 2 due, Assignment 3 issued [A2] [A3]
2/26 Lecture 15 Continuations and Exceptions [Notes][Handout]
Axiomatic Semantics
3/1 Lecture 16 Predicate Transformers [Notes]
3/3 Lecture 17 Hoare Logic [Notes]
3/5 Lecture 18 Dynamic Logic and Kleene Algebra [Notes]
3/8 Lecture 19 Constructions in Dynamic Logic and Kleene Algebra [Notes]
Denotational Semantics
3/10 Lecture 20 Denotational Semantics of IMP [Notes]
3/12 Lecture 21 Denotational Semantics of IMP, cont. [Notes]
3/15 Assignment 3 due [A3]
3/12–3/21 Preliminary Exam
3/15 Lecture 22 Domain Constructions [Notes]
3/17 Lecture 23 Denotational Semantics of REC [Notes]
3/19 Lecture 24 Scott's D Construction [Notes][Handout]
3/20–3/28 Spring Break
3/29 Assignment 4 issued [A4]
Types
3/29 Lecture 25 Typed λ-Calculus [Notes]
3/31 Lecture 26 Soundness of the Typing Rules [Notes]
4/2 Lecture 27 Products, Sums, and Other Datatypes [Notes]
4/5 Lecture 28 Strong Normalization [Notes]
4/7 Lecture 29 Type Inference and Unification [Notes]
4/9 Lecture 30 The Polymorphic λ-Calculus [Notes]
4/12 Lecture 31 Propositions as Types [Notes]
4/14 Lecture 32 Propositions as Types II [Notes][NatDed]
4/16 Assignment 4 due, Assignment 5 issued [A4] [A5]
4/16 Lecture 33 Subtype Polymorphism [Notes]
4/19 Lecture 34 Recursive Types [Notes]
4/21 Lecture 35 Testing Equirecursive Equality [Notes]
4/23 Lecture 36 Coinductive Subtyping of Recursive Types [Notes]
4/26 Lecture 37 Type Inference for Partial Types [Notes]
4/28 Lecture 38 Abstract Interpretation [Notes]
Topics
4/30 Lecture 39 Abstract Interpretation (cont.) [Notes]
5/3 Assignment 5 due [A5]
5/3 Lecture 40 Existential Types [Notes]
5/5 Lecture 41 Object-Oriented Languages [Notes]
5/7 Lecture 42 Monads [Notes][Wadler][Moggi]
5/7–5/17 Final Exam