Logic in Computer Science (LICS 1990)

Paper: Effective domains and intrinsic structure (at LICS 1990)

Authors: Phoa, W.

Abstract

Topos theory is the categorical analog of constructive set theory; and conveniently, PERs (partial equivalence relations) do sit inside a topos-the category of PERs can be (loosely speaking) identified with the full subcategory of modest sets in Hyland's effective topos. (The effective topos is the topos-theoretic version of recursive realizability.) Working in the effective topos is especially attractive since not only can set-theoretic reasoning be used, but one also has a lot of category-theoretic and topos-theoretic machinery at one's disposal. That is the point of view taken in this research. The basic theory of ∑-spaces is discussed. A convex power domain is also presented. Modal operators are outlined. Parallelism and sheaves are examined. Finally, the fixed-point classifier is presented

BibTeX

  @InProceedings{Phoa-Effectivedomainsand,
    author = 	 {Phoa, W.},
    title = 	 {Effective domains and intrinsic structure},
    booktitle =  {Proceedings of the Fifth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1990},
    year =	 1990,
    editor =	 {John Mitchell},
    month =	 {June}, 
    pages =      {366--377},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }