My thesis (Axiomatic Domain Theory in Categories of Partial Maps) is available by anonymous ftp from ftp.dcs.ed.ac.uk directory pub/mf files thesis.dvi.Z and thesis.ps.Z. Marcelo Fiore P.S. The abstract follows: ------------------------------------------------------------------------ Axiomatic Domain Theory in Categories of Partial Maps Marcelo P. Fiore Department of Computer Science Laboratory for Foundations of Computer Science University of Edinburgh, The King's Buildings Edinburgh EH9 3JZ, Scotland <mf@dcs.ed.ac.uk> Phone: + 44 31 650 5145. Fax: + 44 31 667 7209. June 1994 Synopsis 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. ------------------------------------------------------------------------