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 
WellFounded 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 

