This thesis takes up the notion of domain representability introduced
in [Stoltenberg-Hansen, Tucker 95]. The author proves that any
effective metric algebra has an effective domain representation. This
is a very general result extending much beyond the important example of
the real numbers R. To exemplify, the space 
of
continuous real valued functions on the unit interval with the sup norm
is domain representable in an effective way. The domain
representability of metric spaces provides an explanation of the fact
that both domains and metric spaces have been successfully used for
semantics of programming languages. The Banach fixed point theorem for
a complete metric space corresponds in a precise way to the least fixed
point theorem for the representing domain. The author gives a new proof
of a version of Ceitin's theorem for metric spaces - computability
implies continuity - using Berger's generalisation of the
Kreisel-Lacombe-Shoenfield theorem to domains. In order to make this
connection the author needs to weaken the notion of effective domain to
semieffective domain and make a non-trivial use of the fact that a
separable effective metric space has specific representations of both
kinds.
One objective of this paper is the determination of the proof-theoretic strength of Martin-Löf's type theory with a universe and the type of well-founded trees. It is shown that this type system comprehends the consistency of a rather strong classical subsystem of second order arithmetic, namely the one with comprehension and bar induction. This yields a constructive consistency proof of a strong classical theory. Also the proof-theoretic strength of other inductive types like Aczel's type of iterative sets is investigated in various contexts.
In this paper the theory of Scott-Ershov domains is connected to first order model theory. The completeness property of domains is related to the model theoretic notion of saturation. In constraint programming this analogy is already used on the level of finite approximations. A simple relation to structures used in non-standard analysis (ultrapowers, Fréchet powers) is obtained. This leads to natural logical presentations of domain constructions such as function space, products and the Smyth power domain. Sufficient conditions on models for constructing function spaces are given. It is conjectured that the non-standard models will be helpful in the analysis of streams.
The notion of logically presented domains developed in [Palmgren, Stoltenberg-Hansen 95] is used to give a characterisation of the Kleene-Kreisel continuous functionals. Certain logical types, i.e. finitely consistent sets of formulas, over the full type structure built from N correspond to Kleene's associates while the elements realising these types correspond to functionals having associates. To define these --- the total types --- a non-standard extension of the full type structure is made. The set of non-standard elements is sufficiently rich to single out the total types. The logical form of the domain constructions allows the use of a Fréchet power as a non-standard extension. This extension is constructive in the sense that it avoids the use of the axiom of choice.
There are several general ways to deal with effective algebras when
the notion of effectivity is in terms of effective approximations.
One way is via domain representability, worked out for locally compact
Hausdorff algebras in [Stoltenberg-Hansen, Tucker 95] and for metric
algebras in [Blanck 95]. Another way is via the theory of formal
spaces or locales. A general question is: Are these approaches related
and, if they are, to what extent? In particular, what is the
relationship between various notions of totality for domains and points
of a formal space? The paper partly answers these questions by
considering representations of locally compact Hausdorff (and hence
regular) spaces. Given a canonical domain representation over a
conditional upper semilattice P of a locally compact regular space, a
set of generators for a covering relation over P is found which
isolates precisely the total elements (with its usual definition)
of the domain as the points of the formal space. Then another set of
generators is found such that the points of the formal space resulting
from both sets of generators is homeomorphic to the originally given
space. The converse is not true. Given a locally compact regular
formal space 
it is not necessarily true that the points are
total ideals in the domain, the ideal completion of P. For the special
case of locally compact regular formal spaces one may define another
notion of totality in such a way that one obtains a domain
representation in the usual fashion.