NOTE: The current schedule is tentative and subject to change. Nonetheless it gives an idea of the material to be covered in this course. The lecture notes are seeded from previous years, and will be sporadically updated.

Key to readings: P = Pierce; SF = Software Foundations; M = Mitchell; W = Winskel; K = Krishnamurthi 1st ed.; K2nd = Krishnamurthi 2nd ed.; 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 Stephen Chong, Radu Rugina, Andrew Myers, Nate Foster, and Jeff Vaughan.

Videos of the lecture and sections are available on Canvas. The same site also provides a Zoom link for live streaming of and remote participation in lectures.

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 Slides Code Assignments
Semantics
1Tue 26-Jan Intro to semantics, Proof tools P 2.4, 3
SF1-Induction,Imp
SF2-SmallStep
W 2,3,4
H 2
PDF OCaml
Coq
2Thu 28-Jan Small-step semantics PDF PDF Coq
3Tue 2-Feb Induction PDF PDF Coq Assignment 1 released
4Thu 4-Feb Large-step semantics PDF PDF Coq
5Tue 9-Feb IMP: a simple imperative language PDF PDF Coq
6Thu 11-Feb Denotational semantics W 5
M 4.3
PDF PDF
Lambda calculus
7Tue 16-Feb Lambda calculus P 5
M 4.2
K 22
PDF PDF
8Thu 18-Feb Lambda calculus encodings and Recursion PDF PDF
9Tue 23-Feb Definitional translations PDF PDF
10Thu 25-Feb References and continuations P 13
M 5,4, 8.3.2
H 29, 36
K 18-20
PDF PDF Assignment 1 due
Assignment 2 released
Types
11Tue 2-Mar Simply-typed lambda calculus
Type soundness
P 9
SF2-Stlc
SF2-StlcProp
M 6.1, 6.2
K 24-26

(P 12)
(SF2-Norm)

PDF PDF
13Thu 4-Mar More types P 11, 13
SF2-MoreStlc
SF2-References
PDF PDF
12Tue 9-Mar NO CLASS
MIDTERM
14Thu 11-Mar Parameteric Polymorphism, Records and Subtyping P 23
M 6.4
P 11.8, 15
PDF PDF Assignment 3 released
No Class
15Thu 18-Mar Curry-Howard isomorphism; Existential types P 9.4
SF1-ProofObjects
PDF PDF Haskell Assignment 2 due
16Tue 23-Mar Type Inference P 22
K30
PDF PDF Prolog
17Thu 25-Mar Sub-structural type systems PDF PDF eg1.rs
eg2.rs
eg3.rs
eg4.rs
eg5.rs
Assignment 3 due
Assignment 4 released
18Tue 30-Mar Algebraic structures PDF PDF m.hs
agediff.hs
io.hs
state.hs
Reasoning About Programs
19Thu 1-Apr Axiomatic Semantics and Hoare Logic SF2-Hoare
W 6
(W 7)
PDF PDF hoare.c
hoare.dfy
factorial.c
factorial.dfy
20Tue 6-Apr Dependent types PDF PDF Twelf
0Thu 8-Apr Embedded EthiCS: Specifications of Ethical Concerns Assignment 4 due
Assignment 5 released
Misc. Topics
21Tue 13-Apr Logic Programming
(Guest appearance: Will Byrd)
M 15
K32-34
PDF
No Class
22Tue 20-Apr Probabilistic Programming
(Guest lecturer: Yizhou Zhang)
PDF
25Thu 22-Apr Semantics for Verified Software-Hardware Stacks
(Guest lecturer: Samuel Gruetter)
Assignment 5 due
Assignment 6 released
24Tue 27-Apr Concurrency M 14 PDF PDF ex1.go
ex2.go
ex3.go
Thu 29-Apr Assignment 6 due
TBD TBD-May FINAL EXAM: TBD