Department of Computer Science and Technology

Technical reports

Power-domains, modalities and the Vietoris monad

E. Robinson

October 1986, 16 pages

DOIhttps://doi.org/10.48456/tr-98

Abstract

It is possible to divide the syntax-directed approaches to programming language semantics into two classes, “denotational”, and “proof-theoretic”. This paper argues for a different approach which also has the effect of linking the two methods. Drawing on recent work on locales as formal spaces we show that this provides a way in which we can hope to use a proof-theoretical semantics to give us a denotational one. This paper reviews aspects of the general theory, before developing a modal construction on locales and discussing the view of power-domains as free non-deterministic algebras. Finally, the relationship between the present work and that of Winskel is examined.

Full text

PDF (1.1 MB)

BibTeX record

@TechReport{UCAM-CL-TR-98,
  author =	 {Robinson, E.},
  title = 	 {{Power-domains, modalities and the Vietoris monad}},
  year = 	 1986,
  month = 	 oct,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-98.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-98},
  number = 	 {UCAM-CL-TR-98}
}