Denotational Semantics

Achim Jung (Birmingham)

In this course we will focus on the denotational semantics of the simply typed lambda calculus. We aim to show the following results:

  1. the completeness of alpha, beta and eta rules with respect to the set theoretic model over the natural numbers
  2. the adequacy of the Scott model for PCF
  3. Milner's context lemma
Along the way we will discuss the substitution lemma, term models, logical relations, and basic domain theory.

The first part is based on Chapter 2 of the book "Semantics of Programming Languages" by Carl A. Gunter, MIT Press 1992. The other two on "Domain-Theoretic Foundations of Functional Programming" by Thomas Streicher, World Scientific 2006. Both books contain a lot more material than I can present in this course. The same is true for "Foundations for Programming Languages" by John C. Mitchell, MIT Press 1996. The common feature of these three works and my course is that the simply typed lambda calculus is taken as the starting point, whereas other texts on denotational semantics tend to begin with an (imperative) while-language.

A detailed outline of the course together with a rationale for the selection of topics has been published in the ACM SIGLOG News, vol. 1, nr. 2, October 2014, pages 25-37.

Last modified: Wed, 08 February, 2017