Skip to content

Cambridge: Semantics of Programming Languages


  • Offered by: University of Cambridge
  • Prerequisites: elementary Discrete Mathematics, including logic and proof methodology, basic functional programming
  • Programming Languages: OCaml (ML)
  • Difficulty: 🌟🌟🌟
  • Class Hour: 20 to 30 hours (12 hours of lecture)

This course offers a structural, operational approach to programming language semantics. It provides a very beginner-friendly but mathematically rigorous introduction to the constructs and specification declaration of programming languages, in the context of actually defining and designing a language. It is also one of the few PLT courses that offers publicly available videos.

The course covers semantics topics ranging from operational and denotational semantics. The course starts with introducing the basic operational semantics of a simple imperative language defined by BNF, and gradually coming to introducing formal type systems, using mathematical induction (especially structural induction) to build rule-based induction proofs. It then comes to how we manipulate data under a functional programming perspective and introduces subtyping and handling of functions. Finally it comes to the discussion of semantics equivalence, congruence property and semantics under concurrency.

This course was taught to 2nd year undergraduate students, however building up some very important concepts. It would be a pivotal capstone for further studies on type theory, category theory, hoare logic and model checking.

Course Resources

  • Course Website: Latest
  • Recordings: YouTube
  • Textbooks:
  • Pierce, B.C. (2002). Types and programming languages. MIT Press.
  • Winskel, G. (1993). The formal semantics of programming languages. MIT Press.
  • Assignments: Related Past Paper Questions are listed here, however solutions and tutorial sheets are visible to internal students only.