ACTIVITIES

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 University, Copenhagen.)