Continuous Domains in Logical Form
Mathias Kegelmann · Electronic Notes in Theoretical Computer Science · 2002
Abstract This thesis investigates the mathematical foundations that are necessary for an extension of Abramsky's domain theory in logical form to continuous domains. We present a multi-lingual sequent calculus, that is a positive logic allowing sequents that relate propositions from different languages. This setup necessitates a number of syntactic adjustments. In particular, we discuss different reformulations of the cut rule and how they can be used as a basis for a category MLS of logical systems. Then we investigate cut elimination in this logic. From a semantic point of view this can be seen as enabling us to perform domain constructions in purely syntactic form. The category MLS has a number of different manifestations, and we study it with logical, localic, topological and categorical methods. From a topological point of view, we show that MLS is equivalent to the category of stably compact spaces with certain closed relations. By putting together cut elimination and representation theorems for these spaces we get a continuous domain theory in logical form.