NOTE: The current schedule is tentative and subject to change. Nonetheless it gives an idea of the material to be covered in this course.

Key to readings: M = Mitchell; W = Winskel; K = Krishnamurthi 1st ed.; K2nd = Krishnamurthi 2nd ed.; P = Pierce; H = Harper. The readings are not required, but may help your understanding of the lecture material.

The lecture notes here contain material from lecture notes by Radu Rugina, Andrew Myers, Nate Foster, and Jeff Vaughan.

Videos of the lecture and section are available here. The same site also provides live streams for lecture.

For background material on sets, relations, functions, and induction, see: W 1, H 2, H Appendix, and/or P 2.

Lec. Date Topic Readings Notes Assignments
Semantics
1Tue 29-Jan Intro to semantics W 2,3,4
P 2.4, 3
H 2
2Thu 31-Jan Small-step semantics PDF
3Tue 5-Feb Induction PDF
4Thu 7-Feb Large-step semantics PDF Assignment 1 released
5Tue 12-Feb IMP: a simple imperative language PDF
6Thu 14-Feb Denotational semantics W 5
M 4.3
PDF
Lambda calculus
7Tue 19-Feb Lambda calculus P 5
M 4.2
K 22
PDF
8Thu 21-Feb Lambda calculus encodings and Recursion PDF Assignment 1 due
Assignment 2 released
9Tue 26-Feb Definitional translations PDF
10Thu 28-Feb References and continuations P 13
M 5,4, 8.3.2
H 29, 36
K 18-20
PDF
Types
11Tue 5-Mar Simply-typed lambda calculus
Type soundness
P 9
M 6.1, 6.2
K 24-26
PDF
12Thu 7-Mar More types P 11, 13 PDF Assignment 2 due
13Tue 12-Mar MID-TERM EXAM
(Covers lectures 1-10)
Assignment 3 released
14Thu 14-Mar Type inference P 22
K 30
PDF
Spring Recess
15Tue 26-Mar Parameteric Polymorphism, Records and Subtyping P 23
M 6.4
P 11.8, 15
PDF
16Thu 28-Mar Curry-Howard isomorphism; Existential types P 9.4 PDF Assignment 3 due
Assignment 4 released
17Tue 2-Apr Sub-structural type systems PDF
18Thu 4-Apr Algebraic structures PDF
Reasoning About Programs
19Tue 9-Apr Axiomatic Semantics and Hoare Logic PDF
20Thu 11-Apr Dependent types PDF Assignment 4 due
Assignment 5 released
21Tue 16-Apr Proof tools
22Thu 18-Apr Specification of ethical concerns (Embedded EthiCS module)
Guest Lecturer: Diana Acosta Navas
In-person lecture attendance expected
PDF
Misc. Topics
23Tue 23-Apr Logic Programming M 15
K32-34
PDF
24Thu 25-Apr Specification of ethical concerns (Embedded EthiCS module)
Guest Lecturer: Diana Acosta Navas
In-person lecture attendance expected
Assignment 5 due
Assignment 6 released
25Tue 30-Apr Dynamic types PDF
Thu 2-May Assignment 6 due
Thu 9-May FINAL EXAM: 9am-12pm in Science Center D