Every programming language is a small mathematical universe with its own laws: what a program
means, which programs are well-formed, and which are provably safe. Programming-language
theory is the study of those laws — the discipline that lets us say precisely what
\text{if } b \text{ then } e_1 \text{ else } e_2 denotes, prove that a
well-typed program "cannot go wrong", and design new languages whose guarantees are theorems rather
than hopes. It is the most mathematical corner of computer science, and the most quietly influential:
every idea here — from the \lambda-calculus to Hindley–Milner inference to
the Curry–Howard correspondence — is now load-bearing in the languages people use every day.
This master's-level course follows the classic route of Pierce's Types and Programming
Languages, Harper's Practical Foundations for Programming Languages, and Winskel's
The Formal Semantics of Programming Languages. It begins with the metatheory of syntax and
inference rules, builds the untyped and typed \lambda-calculus, develops
the three great styles of semantics (operational, denotational, axiomatic), and then climbs the tower
of type systems — from the simply-typed calculus through parametric polymorphism, subtyping,
recursive and existential types, up to the edge of dependent types — before closing with how these
ideas become real interpreters and compilers. It is a natural companion to
Compiler Design:
that course builds the machine, this one explains what the machine is allowed to assume.
It assumes the undergraduate treatment of
programming languages,
the
automata
and grammars of theory of computation, comfort with
induction, and a little
logic.