Synthetic Domain Theory aims at giving a few simple axioms to be added
to an intuitionistic set theory in order to obtain domain-like sets.
The idea at the core of the study was proposed by Dana Scott in the
late 70's: domains should be certain sets in a
mathematical universe where domain theory would then become available
as part of the set theory; in particular, these domains
come with intrinsic notions of approximation and passage to the limit
with respect to which all functions are continuous.
The properties needed in denotational semantics,
e.g. closure under sums, products, and exponentials, the
admission of fixed-point operators, and the solution of recursive
domain equations come for free from the set theory of the universe.
Researchers at DISI have been directly involved in the early
development of SDT, producing some very important results.
We are now in the process of testing the theory on the construction of
parametric models of the polymorphic lambda calculus with fixed-point
operators which should enable us to prove representation independence
results. Reference to any ad-hoc operational calculus would then be
avoided and any of the models would convey directly the usual,
"simple" (in the sense of "set-theoretical") intuition back on the
programming language in use.
(Collaboration with University of Cambridge, Information Technology