Technical reports

Logics of domains

Guo Qiang Zhang

December 1989, 250 pages

This technical report is based on a dissertation submitted May 1989 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Trinity College.

DOI: 10.48456/tr-185

Abstract

This dissertation studies the logical aspects of domains as used in the denotational semantics of programming languages. Frameworks of domain logics are introduced which serve as basic tools for the systematic derivation of proof systems from the denotational semantics of programming languages. The proof systems so derived are guaranteed to agree with the denotational semantics in the sense that the denotation of any program coincides with the set of assertions true of it.

The study focuses on two frameworks for denotational semantics: the SFP domains, and the less standard, but important, category of dI-domains with stable functions.

An extended form of Scott’s information systems are introduced to represent SFP objects. They provide better understanding of the structure of finite elements and open sets of domains. These systems generalise to a logic of SFP which uses inequational formulae to axiomatise entailment and non-entailment of open-set assertions. Soundness, completeness, and expressiveness results of the logic are obtained, and possible applications are investigated. A μ-calculus of Scott domains is introduced to extend the expressive power of the assertion language.

Special kinds of open sets called stable neighbourhoods are introduced and shown to determine stable functions in a similar sense to that in which Scott-open sets determine continuous functions. Properties and constructions of the stable neighbourhoods on various categories of dI-domains are investigated. Logical frameworks for Girard’s coherent spaces and Berry’s dI-domains are given in which assertions are interpreted as stable neighbourhoods. Various soundness, completeness, and expressiveness results are provided.

Full text

PDF (17.5 MB)

BibTeX record

@TechReport{UCAM-CL-TR-185,
  author =	 {Zhang, Guo Qiang},
  title = 	 {{Logics of domains}},
  year = 	 1989,
  month = 	 dec,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-185.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-185},
  number = 	 {UCAM-CL-TR-185}
}