Schedule

Chapters and sections refer to the class notes. Homework is listed on the day it is assigned and is always due one week later. This schedule is tentative and subject to change during the semester. Comments and suggestions are welcome!

Nr	Date	Topic	Reading	Code	Slides	Assignment
1	Jan 14	Introduction	Ch 1
2	Jan 16	Natural Semantics for Mini-ML	2.1-2.5
3	Jan 21	Type Preservation	2.6-2.7			2.7, 2.11, 2.13
4	Jan 23	Representation in LF	3.1-3.3
5	Jan 28	Judgments as Types	3.4-3.6			3.17
6	Jan 30	Higher-Level Judgments	3.7-3.8
7	Feb 4	An Introduction to Elf	Ch 4	mini-ml		4.2, 4.3
8	Feb 6	Parametric and Hypothetical Judgments	5.1-5.5	mini-ml	Lecture 8
9	Feb 11	Representing Type Preservation	5.6	mini-ml	Lecture 9	5.15
10	Feb 13	Evaluation with Environments	6.1-6.2	compile	Lecture 10
11	Feb 18	A Continuation Machine	6.5-6.6	compile
12	Feb 20	Contextual Evaluation	6.7	compile	Lecture 12	6.14, 6.15, 6.16
13	Feb 25	Constraints in Elf		compile
14	Feb 27	Continuation-Passing Style		compile	Lecture 14
15	Mar 4	Natural Deduction	7.1-7.3	natded	Lecture 15	7.11, 7.12
16	Mar 6	The Curry-Howard Isomorphism	7.4-7.5	natded	Lecture 16
17	Mar 11	Proof Search and Sequent Calculus		sequents	Lecture 17
18	Mar 13	Sequent Calculus and Natural Deduction		sequents	Lecture 18
19	Mar 18	Cut Elimination	Paper	cut-elim	Lecture 19
	Mar 20	Guest Lecture (E. Moggi)
	Mar 25	Spring Break
	Mar 27	Spring Break
20	Apr 1	Uniform Derivations	8.1		Lecture 20
21	Apr 3	Normalization via Logical Relations	8.2
22	Apr 8	Resolution	8.1, 8.5
23	Apr 10	Failure Continuations	8.5, 8.6
24	Apr 15	The Polymorphic Lambda-Calculus
25	Apr 17	Pure Type Systems and Inductive Types	Paper
26	Apr 22	Recursive Types	Paper
27	Apr 24	Termination via Logical Relations
28	Apr 29	Atomic Subtyping		subtypes	Lecture 28
29	May 1	Refinement Types	Paper

fp@cs