1 - Introduction

Summary

The denotational semantics approach to the semantics of programming languages understands the language constructions by assigning elements of mathematical structures to them. The structures form so-called categories of domains and the study of their closure properties is the subject of domain theory [Sco70,Sco82,Plo83a,GS90,AJ94].

Typically, categories of domains consist of suitably complete partially ordered sets together with continuous maps. But, what is a category of domains? Our aim in this thesis is to answer this question by axiomatising the categorical structure needed on a category so that it can be considered a category of domains. Criteria required from categories of domains can be of the most varied sort. For example, we could ask them to

• have fixed-point operators for endomorphisms and endofunctors;

• have a rich collection of type constructors: coproducts, products, exponentials, powerdomains, dependent types, polymorphic types, etc;

• have a Stone dual providing a logic of observable properties [Abr87, Vic89,Zha91];

• have only computable maps [Sco76,Smy77,McC84,Ros86,Pho90a].

The criteria adopted here will be quite modest but rich enough for the denotational semantics of deterministic programming languages. For us a category of domains will be a category with the structure necessary to support the interpretation of the metalanguage FPC (a type theory with sums, products, exponentials and recursive types). And our axiomatic approach will aim not only at clarifying the categorical structure needed on a category for doing domain theory but also at relating such mathematical criteria with computational criteria.