Locally Boolean Domains and Universal Models for Infinitary Sequential Languages
Tobias Löw · Technischen Universität Darmstadt · 2008
In the first part of this Thesis we develop the theory of locally boolean domains and bistable maps and show that the category of locally boolean domains and bistable maps is equivalent to the category of Curien-Lamarche games and observably sequential functions. Further we show that the category of locally boolean domains has inverse limits of ω-chains of embedding/projection pairs. In the second part we consider the category of locally boolean domains and bistable maps as model for functional programming languages: in "Bistable biorders: a sequential domain theory" J. Laird has shown that an infinitary sequential extension of the functional core language PCF has a fully abstract model in the category of locally boolean domains. We introduce an extension SPCF∞ of his language by recursive types and show that it is universal for its model in locally boolean domains. Finally we consider an infinitary target language CPS∞ for the CPS translation presented by B. Reus and T. Streicher in "Classical logic, continuation semantics and abstract machines" and show that it is universal for a model in locally boolean domains which is constructed like Dana Scott's D∞ where D = O = {⊥,⊤}.