What has been missing is a simple connection between domains and the usual set-theoretical structures of mathematics as well as a comprehensive logic to reason about domains and the functions to be defined upon them. In December of 1996, Scott realized that the very old idea of partial equivalence relations on types could be applied to produce a large and rich category containing many specific categories of domains and allowing a suitable general logic. The category is called Equ, the category of equilogical spaces.
The simplest definition is the category of T0-spaces and total equivalence relations with continuous maps that are equivariant (meaning, preserving the equivalence relations). An equivalent definition uses algebraic (or continuous) lattices and partial equivalence relations, together with continuous equivariant maps. This category is not only cartesian closed, but it is locally cartesian closed (that is, it has dependent sums and products). Moreover, it contains as a full subcategory all T0-spaces (and therefore the category of sets and the category of domains).
The logic for this category is intuitionistic and can be explained by a form of the realizability interpretation. The project now is to use this idea as a unifying platform for semantics and reasoning. Our small group of faculty and students at Carnegie Mellon, namely Steven Awodey, Andrej Bauer, Lars Birkedal, and Jesse Hughes, has begun work on this program. A selection of our theses and papers is listed in the bibliography.
Back to Logics of Types and Computation page.