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