Submit via gradescope
- HW1, due Monday, September 22th at midnight
- HW2, due Monday, October 6th at midnight
- HW3, due Monday, October 20th at midnight
- HW4, due Monday, November 10th at midnight
- HW5, due Monday, November 24th at midnight
- HW6, due Monday, December 8th at midnight
The course content is summarized in the Lectures notes.
| Date | Chapter(s) | Lang | Topic |
|---|---|---|---|
| W 8/27 | No Class: Instructor travel | ||
| M 9/1 | No Class: Labor day | ||
| W 9/3 | Ch. 1 | Introduction: Why study Semantics and Types? What is Type Safety? |
|
| M 9/8 | stlc | Preservation and substitution | |
| W 9/10 | Chs. 1-2 | stlc | Progress Natural number recursion |
| M 9/15 | Ch. 3 | stlc | Big step semantics |
| W 9/17 | Ch. 4 | stlc | Semantic soundness |
| M 9/22 | Ch. 5 | rec | HW #1 due Recursive definitions |
| W 9/24 | rec | Metatheory of recursive definitions | |
| M 9/29 | Ch. 6 | rec | Semantic soundness with recursive definitions |
| W 10/1 | rec | Step-indexed logical relations | |
| M 10/6 | rec | HW #2 due More step-indexed logical relations |
|
| W 10/8 | rec | More step-indexing, Working in Rocq | |
| M 10/13 | Ch. 7 | div | Type-and-effect systems (nontermination) |
| W 10/15 | div | Syntax directed systems, Nontermination Monad | |
| M 10/20 | Ch. 8 | modal | HW #3 due Nontermination monad |
| W 10/22 | modal | More nontermination monad | |
| M 10/27 | Midterm Exam (in class) | ||
| W 10/29 | Ch. 9 | rec | Explicit control stacks |
| M 11/3 | Ch. 10.1 | control | Exceptions |
| W 11/5 | Ch. 10.2 | control | Continuations |
| M 11/10 | Ch. 10.3 | control | HW #4 due Effect handler examples |
| W 11/12 | control | Semantics of effect handlers | |
| M 11/17 | Ch. 10.2 | control | CPS conversion |
| W 11/19 | PFPL Ch. 13 | Classical Logic | |
| M 11/24 | Ch. 11 | untyped | HW #5 due Untyped program equivalence definitions |
| W 11/26 | No Class: Friday schedule for Thanksgiving | ||
| M 12/1 | untyped | Untyped program equivalence examples | |
| W 12/3 | untyped | Untyped program equivalence proofs | |
| M 12/8 | Ch. 12 | rec | HW #6 due Typed program equivalence |
| T 12/16 | Final exam: Tuesday, December 16, 2025: 9:00am to 11:00am in TOWNE 305 |
-
Participation (10%): This is a new, experimental class and everyone in the class will be co-developers. As a result, you are expected to actively contribute. This mainly means being a part of the lectures by ask questions, thinking about puzzles, participating in the discussion, and generally volunteering your insights and reactions. You can also participate by chatting during office hours or submitting pull-requests on the lecture notes. Let me know if you are sick or otherwise need to miss class.
-
Homework (40%): There will be six homework assignments throughout the semester. These will involve written proofs, with opportunities for machine assistance. These assignments are designed to solidify your understanding of the core concepts.
-
Midterm Exam (20%): 90 minute in-class exam sometime in October.
-
Final Exam (30%): 2-hour exam during the final exam period.
You will need to typeset your assignments solutions using LaTeX. Starter code will be provided to save you time.
The purpose of homework assignments is to give you practice with the concepts, force you think closely about the details, and receive feedback about your progress.
You can collaborate on your assignments, but you must submit your own work. I encourage you to discuss the homework problems with your classmates.
You must cite all sources that you use to the complete the assignments. If you discuss the assignment with anyone, list their name. If you refer to online textbooks, lecture notes, etc. please include a link. If you use a LLM or AI tool, provide a short description of what tool you used and how it helped you.
Note that really good homework exercises that help you practice with the material are hard to come by. The exercises for this semester will be variations of problems that I've seen before and have experience with. That means that you will probably be able to find solutions via web search or asking LLMs to solve the problems for you.