*Abstract:*

This thesis is an investigation into *axiomatic categorical
domain theory* as needed for the denotational semantics of
deterministic programming languages.

To provide a direct semantic treatment of non-terminating
computations, we make partiality the core of our theory. Thus, we
focus on categories of partial maps. We study representability of
partial maps and show its equivalence with classifiability. We
observe that, once partiality is taken as primitive, a notion of
approximation may be derived. In fact, two notions of
approximation, contextual approximation and specialisation, based
on testing and observing partial maps are considered and shown to
coincide. Further we characterise when the approximation relation
between partial maps is domain-theoretic in the (technical) sense
that the category of partial maps **Cpo**-enriches with respect
to it.

Concerning the semantics of type constructors in categories of
partial maps, we present a characterisation of colimits of diagrams
of total maps; study order-enriched partial cartesian closure; and
provide conditions to guarantee the existence of the limits needed
to solve recursive type equations. Concerning the semantics of
recursive types, we motivate the study of enriched algebraic
compactness and make it the central concept when interpreting
recursive types. We establish the fundamental property of
algebraically compact categories, namely that recursive types on
them admit canonical interpretations, and show that in
algebraically compact categories recursive types reduce to
inductive types. Special attention is paid to **Cpo**-algebraic
compactness, leading to the identification of a 2-category of kinds
with very strong closure properties.

As an application of the theory developed, enriched categorical
models of the metalanguage FPC (a type theory with sums, products,
exponentials and recursive types) are defined and two abstract
examples of models, including domain-theoretic models, are
axiomatised. Further, FPC is considered as a programming language
with a call-by-value operational semantics and a denotational
semantics defined on top of a categorical model. Operational and
denotational semantics are related via a computational soundness
result. The interpretation of FPC expressions in domain-theoretic
**Poset**-models is observed to be representation-independent.
And, to culminate, a computational adequacy result for an
axiomatisation of absolute non-trivial domain-theoretic models is
proved.

**PhD Thesis - Price £9.00**

This is a 282 page PhD thesis which is available as a DVI file (1Mb) and as a PostScript file (1.6Mb).

*LFCS report ECS-LFCS-94-307 (also published as CST-113-94),
August 1994.*