Universality Results for Models in Locally Boolean Domains

Abstract. In [6] J. Laird has shown that an infinitary sequential extenPCF has a fully abstract model in his category of locally boolean domains (introduced in [8]). In this paper 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 (of [16]) and show that it is universal for a model in locally boolean domains which is constructed like Dana Scott's D where D = {, }.

• Type: Conference
• Year: 2006
• Where: CSL
• Authors: Tobias Löw, Thomas Streicher
• Keywords: Automated Reasoning, Boolean Domains, CSL 2006, Infinitary Sequential ExtenPCF, Infinitary Target Language