Introduction to Domain Theory

Graham Hutton, University of Nottingham

Overview

Domain theory has its roots in the seminal work of Scott and Strachey in the 1970s on denotational semantics, in particular on solving the technical problems that arise in giving semantics to recursively defined programs and types. As well as being one of the most fascinating topics in the foundations of computing science, domain-theoretic ideas are used in many branches of modern research on programming languages and their semantics.

The aim of this course is to teach the basic concepts of domain theory.

Lectures

1. Introduction (denotational semantics, non-termination and bottom, partially-ordered sets, monotonic functions);
   
   
2. Recursively defined programs (chains, directed sets, least upper bound, cpos and continuous functions, the fixpoint theorem);
   
   
3. Constructions on cpos (sums, products, function-spaces, lifting, lazyness vs strictness, axiomatisations, functors);
   
   
4. Scott domains (finite elements, algebraicity, a representation theorem, consistent completeness, Scott-domains);
   
   
5. Recursively defined domains (colimits, cocontinuous functors, the generalised fixpoint theorem, Scott's inverse limit construction, modelling the untyped lambda-calculus).

Summary

There is also a summary sheet of the main concepts from lectures 1-4.