Winter School on Denotational Semantics
The school will be carried out in English, attendance is free of charge, but the number of participants is potentially limited. The exact time and venue will be announced later.
To register for the school and receive future announces please join the following group:
Summary: In this course we will focus on the denotational semantics of the simply typed lambda calculus. We will in parallel introduce enough of the lambda calculus so that the course is accessible to those also who have not studied it in detail before. (In any case, for us the lambda calculus is just a very concise way of writing programs in a functional language.)
We aim to show the following results:
- the completeness of alpha, beta and eta rules with respect to the set theoretic model over the natural numbers;
- the adequacy of the Scott model for PCF;
- Milner's context lemma;
- modelling the untyped calculus.
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.
The 1st Lecture
The 2nd Lecture
The 3rd Lecture
The 4th Lecture
The 5th Lecture
The 6th Lecture
The 7th Lecture
The 8th Lecture
The 9th Lecture
The 10th Lecture