Denotational semantics is concerned with the mathematical meaning of programming languages. Programs are to be interpreted in categories with structure by which we mean initially sets and functions, and later, suitable topological spaces and continuous functions. The main goals of this branch of computer science are, in our belief:

• To provide rigorous definitions that abstract away from implementation details, and that can serve as an implementation independent reference.

• To provide mathematical tools for proving properties of programs: as in logic, semantic models are guides in designing sound proof rules, that can then be used in automated proof-checkers like LCF.

Historically the first goal came first. In the sixties Strachey was writing semantic equations involving recursively defined data types without knowing if they had mathematical solutions. Scott provided the mathematical framework, and advocated its use in a formal proof system called LCF. Thus denotational semantics has from the beginning been applied to the two goals.

In this book we aim to present in an elementary and unified way the theory of certain topological spaces, best presented as order theoretical structures, that have proved to be useful in the modelling of various families of typed λ-calculi considered as core programming languages and as meta-languages for denotational semantics. This theory is now known as Domain Theory, and has been founded as a subject by Scott and Plotkin.

The notion of continuity used in domain theory finds its origin in recursion theory.