In this course we will focus on the denotational semantics of the simply typed lambda calculus. We aim to show the following results:
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.