CISC 465/3.0 Semantics of Programming Languages
Original Author: Joshua Dunfield
Last Revised: 2019-03-20
Specifying syntax and semantics; operational and denotational semantics.
Lambda calculi, type systems and logical foundations.
Semantics of imperative languages.
Registration in a School of Computing plan
(CISC 204/3.0 and CISC 223/3.0 and CISC 360/3.0)
Learning hours: 120 (36L; 84P)
This course satisfies a requirement of the
focus of the COMP degree plan.
B.C. Pierce. Types and Programming Languages (2002). MIT Press.
G. Winskel. The formal semantics of programming languages: an introduction (1993). MIT Press.
R. Harper. Practical Foundations for Programming Languages (2016). Cambridge University Press.
grammars, rules and derivations (1 week)
typed lambda calculi; big-step and small-step semantics (2 weeks)
logical foundations: Gentzen's natural deduction, sequent calculus, the Curry–Howard correspondence (3 weeks)
meta-theoretic properties: induction on derivations; logical soundness and completeness; type preservation and progress (2 weeks)
subtyping and polymorphism (1 week)
semantics of imperative languages: effects and state (1 week)
denotational semantics and domain theory (1 week)
1 week reserve for tests and advanced topics