{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:27:21Z","timestamp":1761611241147},"reference-count":10,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T00:00:00Z","timestamp":1236124800000},"content-version":"unspecified","delay-in-days":5482,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[1994,3]]},"abstract":"<jats:p>In a PCF-like call-by-name typed \u03bb-calculus with a minimal fixpoint operator, \u2018parallelor\u2019, Plotkin's \u2018continuous existential quantifier\u2019 \u2203 and recursive types together with constructors and destructors, all computable objects can be denoted by terms of the programming language. According to A. Meyer's terminology (<jats:italic>cf<\/jats:italic>. Meyer (1988)), such a programming language is called <jats:italic>universal<\/jats:italic> in the sense that any extension of it must be conservative, as all computable objects can already be expressed by program terms.<\/jats:p><jats:p>As a byproduct, we get that, in principle, recursive types could be totally avoided, as they appear as syntactically expressible retracts of the non-recursive type <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S0960129500000384_xs1D4A9\" \/> \u2192 <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S0960129500000384_xs1D4D1\" \/>, where <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S0960129500000384_xs1D4A9\" \/> and <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S0960129500000384_xs1D4D1\" \/> are the flat domains of natural numbers and boolean values, respectively.<\/jats:p>","DOI":"10.1017\/s0960129500000384","type":"journal-article","created":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T04:01:18Z","timestamp":1236139278000},"page":"111-115","source":"Crossref","is-referenced-by-count":7,"title":["A universality theorem for PCF with recursive types, parallel-or and \u2203"],"prefix":"10.1017","volume":"4","author":[{"given":"Thomas","family":"Streicher","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2009,3,4]]},"reference":[{"key":"S0960129500000384_ref010","volume-title":"Informal Proceedings of Workshop on Semantics of Programming Languages","author":"Streicher","year":"1983"},{"key":"S0960129500000384_ref008","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90045-7"},{"key":"S0960129500000384_ref006","volume-title":"Theory of Recursive Functions and Effective Computability","author":"Rogers","year":"1967"},{"key":"S0960129500000384_ref004","article-title":"Tw as a universal domain","volume":"17","author":"Plotkin","year":"1978","journal-title":"JCSS"},{"key":"S0960129500000384_ref003","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"S0960129500000384_ref001","doi-asserted-by":"crossref","unstructured":"Kanda A. (1980) Fully Effective Solutions of Recursive Domain Equations, Ph.D. Thesis, Univ. Warwick.","DOI":"10.1007\/3-540-09526-8_30"},{"key":"S0960129500000384_ref009","volume-title":"Scott Domains, Computability and the Definability Problem","author":"Streicher","year":"1982"},{"key":"S0960129500000384_ref005","volume-title":"Lecture Notes","author":"Plotkin","year":"1983"},{"key":"S0960129500000384_ref007","doi-asserted-by":"publisher","DOI":"10.1007\/BF01876321"},{"key":"S0960129500000384_ref002","volume-title":"Proc. LICS'88","author":"Meyer","year":"1988"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129500000384","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T15:03:22Z","timestamp":1557932602000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129500000384\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,3]]},"references-count":10,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1994,3]]}},"alternative-id":["S0960129500000384"],"URL":"https:\/\/doi.org\/10.1017\/s0960129500000384","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,3]]}}}