# Denotational Semantics

## Lecturer

Achim Jung, University of Birmingham
## Abstract

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