Queen's School of Computing

CISC 465/3.0 Semantics of Programming Languages

Original Author: Joshua Dunfield
Last Revised: 2019-03-20

Calendar Description

Specifying syntax and semantics; operational and denotational semantics. Lambda calculi, type systems and logical foundations. Meta-theoretic properties. Semantics of imperative languages.

Prerequisites: Registration in a School of Computing plan and C– in (CISC 204/3.0 and CISC 223/3.0 and CISC 360/3.0)

Learning hours: 120 (36L; 84P)

Degree Planning

  • This course satisfies a requirement of the Fundamental Computation focus of the COMP degree plan.

Possible Texts

  • 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.

Topics

  • 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