Denotational Semantics


Achim Jung, University of Birmingham


The course will concentrate on building models for various lambda calculi. We will first interpret the simply typed lambda calculus in set-based models (also known as Henkin models). We will prove Friedman's Theorem which says that two simply typed lambda terms are \alpha \beta \eta equivalent if and only if they have the same interpretation in all Henkin models.

In the second part we will add some constants to the simply typed lambda calculus which will give rise to a language very similar to the functional part of ML (known as PCF). Because of the presence of recursion we will need to build our models using so-called "domains". The course will therefore introduce these structures and highlight some of the key properties which are necessary for proving "adequacy" of the model.

If there is time, we will also consider lambda calculi with recursive types and a version of the untyped lambda calculus. In order to deal with this, our domain theory will have to be extended with solutions to recursive domain equations.

Thorsten Altenkirch
Last modified: Thu Jan 29 12:24:11 GMT 2004