Schedule
This schedule records the public outline of the Spring 2026 offering.
Date |
| Topic |
| Notes |
Jan 27 |
| Snow week |
| No class |
Jan 29 |
| Snow week |
| No class |
Feb 3 |
| Introduction and Overview |
| |
Feb 5 |
| Operational Semantics |
| |
Feb 10 |
| Introduction to Lean; Operational Semantics in Lean |
| Due: Paper reading proposal |
Feb 12 |
| Proving Semantics Equivalences |
| |
Feb 17 |
| Stack machine |
| |
Feb 19 |
| Compiler Correctness for Arithmetic |
| Due: Paper write-up |
Feb 24 |
| Variables and binding |
| Due: Inductive proof exercise |
Feb 26 |
| Type Systems |
| |
Mar 3 |
| Semantic Type Soundness |
| |
Mar 5 |
| Function Definitions and Calls |
| |
Mar 10 |
| Tuples and Projections; Heaps and Pointers |
| |
Mar 12 |
| Lambda: Syntax, Semantics, Types |
| Due: Type soundness proof exercise |
Mar 17 |
| Spring Break |
| No class |
Mar 19 |
| Spring Break |
| No class |
Mar 24 |
| Termination via Logical Relation |
| |
Mar 26 |
| Type Inferece; Principal Types; Unification |
| |
Mar 31 |
| Compiling Lambda |
| |
Apr 2 |
| Compiler Correctness for Functions |
| Due: Extended type soundness proof exercise |
Apr 7 |
| Compiler Correctness for Functions |
| |
Apr 9 |
| Project Overview |
| |
Apr 14 |
| Compiler Correctness for Functions |
| |
Apr 16 |
| Recursive Types; Type Soundness via Step-Indexed Logical Relation |
| |
Apr 21 |
| Special Topic: GTLC |
| |
Apr 23 |
| Gradual Guarantees |
| |
Apr 28 |
| Gradual Type Inference |
| |
Apr 30 |
| Prinicipal Gradual Typings |
| |
May 5 |
| Safe Gradual Type Migration |
| |
May 7 |
| Wrap-up |
| |
May 14 |
| Final exam period |
| Thursday, May 14, 2026, 10:30am-12:30pm |