{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T17:38:40Z","timestamp":1648921120928},"reference-count":24,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T00:00:00Z","timestamp":1236124800000},"content-version":"unspecified","delay-in-days":6028,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[1992,9]]},"abstract":"<jats:p>In this paper we study partial equivalence relations (PERs) over graph models of the \u03bbcalculus. We define categories of PERs that behave like predomains, and like domains. These categories are <jats:italic>small<\/jats:italic> and <jats:italic>complete<\/jats:italic>; so we can solve domain equations and construct polymorphic types inside them. Upper, lower and convex powerdomain constructions are also available, as well as interpretations of subtyping and bounded quantification. Rather than performing explicit calculations with PERs, we work inside the appropriate <jats:italic>realizability topos<\/jats:italic>: this is a model of constructive set theory in which PERs, can be regarded simply as special kinds of sets. In this framework, most of the definitions and proofs become quite smple and attractives. They illustrative some general technicques in \u2018synthetic domain theory\u2019 that rely heavily on category theory; using these methods, we can obtain quite powerful results about classes of PERs, even when we know very little about their internal structure.<\/jats:p>","DOI":"10.1017\/s0960129500001481","type":"journal-article","created":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T04:02:39Z","timestamp":1236139359000},"page":"277-299","source":"Crossref","is-referenced-by-count":3,"title":["Building domains from graph models"],"prefix":"10.1017","volume":"2","author":[{"given":"Wesley","family":"Phoa","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2009,3,4]]},"reference":[{"key":"S0960129500001481_ref024","unstructured":"Taylor P. (1991) The fixed point property in synthetic domain theory. In: Proc. of 6th Annual Symposim on Logic in Computer Science."},{"key":"S0960129500001481_ref022","unstructured":"Rosolini G. (to appear) About modest sets."},{"key":"S0960129500001481_ref001","unstructured":"Abadi M. and Plotkin G. (1990) A PER model of polymorphism and recursive types. In: proc. of 5th Annual Symposium on Logic in Computer Science."},{"key":"S0960129500001481_ref021","volume-title":"Lecture Notes in Computer Science","volume":"283","author":"Rosolini","year":"1987"},{"key":"S0960129500001481_ref018","unstructured":"phoa W. K.-S. and Taylor P. (preprint) The synthetic Plotkin Powerdomain."},{"key":"S0960129500001481_ref013","unstructured":"phoa W. K.-S. (1990c) Reflectivity for categories of synthetic domains, draft."},{"key":"S0960129500001481_ref008","first-page":"137","volume-title":"Contemp. Math.","volume":"92","author":"Hyland","year":"1987"},{"key":"S0960129500001481_ref007","volume-title":"Category Theory Proceedings, Como 1990","author":"Hyland"},{"key":"S0960129500001481_ref005","volume-title":"The L. E. J. Brouwer Centenary Symposium","author":"Hyland","year":"1982"},{"key":"S0960129500001481_ref004","unstructured":"Freyd P. , Mulry P. , Rosolini G. and Scott D.S. (1990) Extensional PERs. In: Proc. of 5th Annual Symposium on Logic in Computer Science."},{"key":"S0960129500001481_ref002","volume-title":"The Lambda-Calculus: Its Syntax and Semantics","author":"Barendregt","year":"1984"},{"key":"S0960129500001481_ref023","doi-asserted-by":"publisher","DOI":"10.1137\/0205037"},{"key":"S0960129500001481_ref020","unstructured":"Robinson E. (1989) How complete is PER? In: Proc. of 4th Annual Symposium on Logic in Computer Science."},{"key":"S0960129500001481_ref014","volume-title":"Springer Lecture Notes in Computer Science","volume":"526","author":"phoa","year":"1991"},{"key":"S0960129500001481_ref016","volume-title":"Using fibrations to understand subtypes, to appear in Proc. of the Durham Symposum on Applications of Category Theory to Computer Science","author":"phoa","year":"1991"},{"key":"S0960129500001481_ref019","volume":"11","author":"plotkin","year":"1982","journal-title":"SIAM J. Comput."},{"key":"S0960129500001481_ref012","unstructured":"Phoa W. K.-S. (1990b) Domain Theory in Realizability Toposes, Thesis, University of Cambridge; available as CST-82\u201391\/ECS-LFCS-91\u2013171, Department of Computer Science, University of Edinburgh."},{"key":"S0960129500001481_ref006","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(88)90018-8"},{"key":"S0960129500001481_ref003","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-68952-9"},{"key":"S0960129500001481_ref011","unstructured":"Longo G. and Moggi E. (1990) Constructive natural deduction and its \u201c\u03c9-set\u201d interpretation, LIENS-90\u201321, 10 1990; to appear in Math. Structure in Comp. Science."},{"key":"S0960129500001481_ref015","volume-title":"Springer Lecture Notes in Computer Science","author":"phoa","year":"1991"},{"key":"S0960129500001481_ref010","volume-title":"Topos Theory","author":"Johnstone","year":"1977"},{"key":"S0960129500001481_ref017","unstructured":"phoa W. K.-S. (in preparation b) PCF and the untyped \u03bb-calculus."},{"key":"S0960129500001481_ref009","first-page":"60","volume":"3","author":"Hyland","year":"1990","journal-title":"Proc. Lond. Math. Soc."}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129500001481","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T16:49:38Z","timestamp":1558025378000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129500001481\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,9]]},"references-count":24,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1992,9]]}},"alternative-id":["S0960129500001481"],"URL":"https:\/\/doi.org\/10.1017\/s0960129500001481","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992,9]]}}}