Winter School on Denotational Semantics (30 January - 3 February, 2017)

5899f20d0bf5e.jpg

Instructor: prof. Achim Jung, University of Birmingham, UK.

General Information

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:

https://groups.google.com/forum/#!forum/jbr_winter...

Synopsis

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.

School Materials

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