Lectures: TBD
Office Hours: TBD
Instructor: rainoftime
Teaching assistant: TBD
This course explores the theoretical foundations of programming languages, focusing on language design principles, semantics, and type systems. Students will develop a deep understanding of how programming languages are defined and reasoned about formally. The course covers various semantic frameworks, lambda calculus, type systems, and modern language features.
Prerequisites: Basic knowledge of discrete mathematics, algorithms, and experience with at least one programming language. Prior exposure to functional programming is helpful but not required.
| Week | Topic | Description | Readings (S=SF, P=PFPL) |
|---|---|---|---|
| 1 | Introduction | Course overview, history of programming languages, paradigms, and language design principles | P: Ch. 1 |
| 2 | Mathematical Foundations | Sets, relations, functions, induction, logic | S: Basics, P: Ch. 2 |
| 3 | Operational Semantics | Small-step and big-step semantics, evaluation contexts, abstract machines | P: Ch. 3-4, S: Imp, Winskel: Ch. 2-4 |
| 4 | Denotational Semantics | Fixed points, compositionality, basic model theory | P: Ch. 5, Winskel: Ch. 5-8 |
| 5 | Axiomatic Semantics | Hoare logic, weakest preconditions, basic proof theory | S: Hoare Logic, P: Ch. 6, Winskel: Ch. 12 |
| 6 | Lambda Calculus | Untyped lambda calculus, alpha/beta/eta equivalence, Church encodings, evaluation strategies | P: Ch. 8-9, S: LF |
| 7 | Simple Typed Lambda Calculus | Strong normalizability, progress and preservatio | P: Ch. 10-11, S: STLC |
| 8 | Midterm Exam | Review and assessment of course material covered so far | All previous readings |
| 9 | System F | Parametric polymorphism, impredicativity, Reynolds abstraction theorem | P: Ch. 18-19, S: Poly |
| 10 | Type Inference | Hindley-Milner type system, unification, principal types | P: Ch. 20, S: InferWithError |
| 11 | Refinement Types | Liquid types, SMT solving, automated verification | P: Ch. 30, Vazou et al. (2014) |
| 12 | Algebraic Effects (?) | Effect systems, handlers, monads, delimited continuations | Plotkin & Pretnar (2009) |
| 13 | Expression Problem | Extensibility challenges, visitor pattern, type classes, object algebras | Cook (1990), Oliveira & Cook (2012) |
| 14 | Gradual Typing | Type dynamics, blame calculus, hybrid typing, optional typing, performance | Siek & Taha (2006), P: Ch. 27 |
| 15 | TBD | TBD | |
| 16 | Project Presentations & Review | Final project presentations and comprehensive course review |