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.

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 23-Jan Intro to semantics W 2,3,4
P 2.4, 3
H 2
PDF
2Thu 25-Jan Small-step semantics PDF
3Tue 30-Jan Induction PDF
4Thu 1-Feb Large-step semantics PDF Assignment 1 released
5Tue 6-Feb IMP: a simple imperative language PDF
6Thu 8-Feb Denotational semantics W 5
M 4.3
PDF
Lambda calculus
7Tue 13-Feb Lambda calculus P 5
M 4.2
K 22
PDF
8Thu 15-Feb Lambda calculus encodings and Recursion PDF Assignment 1 due
Assignment 2 released
9Tue 20-Feb Definitional translations
Guest lecturer: Anitha Gollamudi
PDF
10Thu 22-Feb References and continuations P 13
M 5,4, 8.3.2
H 29, 36
K 18-20
PDF
Types
11Tue 27-Feb Simply-typed lambda calculus
Type soundness
P 9
M 6.1, 6.2
K 24-26
PDF Assignment 2 due
12Thu 1-Mar MID-TERM EXAM
(Covers lectures 1-10)
Assignment 3 released
13Tue 6-Mar More types P 11, 13 PDF
14Thu 8-Mar Type inference P 22
K 30
PDF
Spring Recess
15Tue 20-Mar Parameteric Polymorphism, Records and Subtyping P 23
M 6.4
P 11.8, 15
PDF
16Thu 22-Mar Curry-Howard isomorphism; Existential types P 9.4 PDF Assignment 3 due
Assignment 4 released
17Tue 27-Mar Sub-structural type systems PDF
18Thu 29-Mar Algebraic structures PDF
Reasoning About Programs
19Tue 3-Apr Axiomatic Semantics and Hoare Logic PDF
20Thu 5-Apr Dependent types PDF Assignment 4 due
Assignment 5 released
21Tue 10-Apr Proof tools
22Thu 12-Apr Ethics in CS
Guest lecturer: David Gray Grant
Readings:
Logic Programming
23Tue 17-Apr Logic Programming M 15
K32-34
PDF
Concurrency
24Thu 19-Apr Dynamic types PDF Assignment 5 due
Assignment 6 released
25Tue 24-Apr Semantics of Concurrency PDF
Thu 26-Apr Assignment 6 due