{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,12,15]],"date-time":"2024-12-15T09:40:15Z","timestamp":1734255615766,"version":"3.30.2"},"reference-count":32,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":5323,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[1999]]},"DOI":"10.1016\/s1571-0661(04)00105-7","type":"journal-article","created":{"date-parts":[[2004,2,5]],"date-time":"2004-02-05T10:34:35Z","timestamp":1075977275000},"page":"74-100","source":"Crossref","is-referenced-by-count":13,"title":["Matching typed and untyped realizability"],"prefix":"10.1016","volume":"23","author":[{"given":"John","family":"Longley","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)00105-7_NEWBIB1","unstructured":"S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF. Accepted for publication, 1996"},{"year":"1985","series-title":"Foundations of Constructive Mathematics","author":"Beeson","key":"10.1016\/S1571-0661(04)00105-7_NEWBIB2"},{"key":"10.1016\/S1571-0661(04)00105-7_NEWBIB3","doi-asserted-by":"crossref","unstructured":"A. Bucciarelli and T. Ehrhard. Sequentiality and strong stability. In Proc. 6th Annual Symposium on Logic in Computer Science, pages 138\u2013145. IEEE, 1991","DOI":"10.1109\/LICS.1991.151638"},{"issue":"2","key":"10.1016\/S1571-0661(04)00105-7_NEWBIB4","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1006\/inco.1994.1047","article-title":"Fully abstract semantics for observably sequential languages","volume":"111","author":"Cartwright","year":"1994","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(04)00105-7_NEWBIB5","unstructured":"M.H. Escardo. A metric model of PCF. Draft paper, March 1999"},{"key":"10.1016\/S1571-0661(04)00105-7_NEWBIB6","doi-asserted-by":"crossref","unstructured":"J.M.E. Hyland. The effective topos. In The L.E.J. Brouwer Centenary Symposium. North-Holland, 1982.","DOI":"10.1016\/S0049-237X(09)70129-6"},{"key":"10.1016\/S1571-0661(04)00105-7_NEWBIB7","unstructured":"J.M.E. Hyland, and C.-H.L. Ong. On full abstraction for PCF: I, II and III. Accepted for publication, 1996"},{"key":"10.1016\/S1571-0661(04)00105-7_NEWBIB8","doi-asserted-by":"crossref","unstructured":"R. Kanneganti, R. Cartwright, and M. Felleisen. SPCF: its model, calculus, and computational power. In Proc. REX Workshop on Semantics and Concurrency","DOI":"10.1007\/3-540-56596-5_39"},{"key":"10.1016\/S1571-0661(04)00105-7_NEWBIB9","doi-asserted-by":"crossref","DOI":"10.2307\/2269016","article-title":"On the interpretation of intuitionistic number theory","volume":"10","author":"Kleene","year":"1945","journal-title":"Journal of Symbolic Logic"},{"year":"1965","series-title":"The Foundations of Intuitionistic Mathematics","author":"Kleene","key":"10.1016\/S1571-0661(04)00105-7_NEWBIB10"},{"key":"10.1016\/S1571-0661(04)00105-7_NEWBIB11","unstructured":"J. Laird. A Semantic Analysis of Control. Ph D thesis, University of Edinburgh, 1998. Examined March 1999."},{"key":"10.1016\/S1571-0661(04)00105-7_NEWBIB12","unstructured":"J.R. Longley. Realizability Toposes and Language Semantics. Ph D thesis, University of Edinburg, 1995. Available as ECS-LFCS-95\u2013332."},{"key":"10.1016\/S1571-0661(04)00105-7_NEWBIB13","unstructured":"J.R. Longley. Realizability; models for sequential computation. In preparation; draft available from the author's home page, 1998."},{"key":"10.1016\/S1571-0661(04)00105-7_NEWBIB14","unstructured":"J.R. Longley. The sequentially realizable functionals. Technical Report ECSLFCS-98\u2013402, Department of Computer Science, University of Edinburgh, 1998. Submitted to Annals of Pure and Applicd Logic."},{"key":"10.1016\/S1571-0661(04)00105-7_NEWBIB15","doi-asserted-by":"crossref","unstructured":"J.R. Longley. Unifying typed untyped realizability. Electronic note, available at http:\/\/www.dcs.ed.ac.uk\/home\/jrl\/unifying.txt, 1999.","DOI":"10.1016\/S1571-0661(04)00105-7"},{"key":"10.1016\/S1571-0661(04)00105-7_NEWBIB16","doi-asserted-by":"crossref","unstructured":"J.R. Longley. When is a functional kprogram not a functional program not a functional program? Accepted for ICFP'99; available from the author's home page, 1999.","DOI":"10.1145\/317636.317775"},{"key":"10.1016\/S1571-0661(04)00105-7_NEWBIB17","unstructured":"J.R Longley and G.D. Plotkin. Logical full abstraction and PCF. In J. Ginzburg et al., editor, Tbilisi Symposium on Languafge, Logic and Computation, pages 333\u2013352. SiLLI\/CSLI, 1997."},{"key":"10.1016\/S1571-0661(04)00105-7_NEWBIB18","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1017\/S0960129597002387","article-title":"A uniform approach to domain theory in realizability models","volume":"7","author":"Longley","year":"1997","journal-title":"Mathematical Structures in Computer Science"},{"key":"10.1016\/S1571-0661(04)00105-7_NEWBIB19","unstructured":"M. Marz, A. Rohr, and T. Streicher. Full abstraction via realisability. In Proc. 14th Annual IEEE Symposium on SLogic in Computer Science, IEEE, 1999."},{"key":"10.1016\/S1571-0661(04)00105-7_NEWBIB20","doi-asserted-by":"crossref","unstructured":"H. Nickau. Hereditarily sequential functionals. In Proc. 3rd Symposium on Logical Foundations of Computer Science, Lecture Notes in Computer Science 813, pafges 253\u2013264. Springer, 1994.","DOI":"10.1007\/3-540-58140-5_25"},{"key":"10.1016\/S1571-0661(04)00105-7_NEWBIB21","doi-asserted-by":"crossref","unstructured":"C.-H.L. Ong and C.A. Stewart. A Curryk-Howard foundation for functional computation with control. In Proc. Symposium on Principles of Programming Languages, lkpages 215\u2013227, ACM Press, 1997.","DOI":"10.1145\/263699.263722"},{"key":"10.1016\/S1571-0661(04)00105-7_NEWBIB22","unstructured":"J. van Oosten. Extensional realizability. Technical Report ML-93-18, University of Amsterdam, ILLC, 1993."},{"key":"10.1016\/S1571-0661(04)00105-7_NEWBIB23","unstructured":"J. van Oosten. A combinatory algebra for sequential functionals of finite type. Technical Report 996, University of Utrecht, 1997. To appear in Proc. Logic Colliquium, Leeds."},{"issue":"289","key":"10.1016\/S1571-0661(04)00105-7_NEWBIB24","article-title":"The modified realizability topos","volume":"116","author":"van Oosten","year":"1997","journal-title":"Journal of Pure and Applied Algebra"},{"key":"10.1016\/S1571-0661(04)00105-7_NEWBIB25","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/0304-3975(77)90044-5","article-title":"LCF considered as a programming language","volume":"5","author":"Plotkin","year":"1977","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)00105-7_NEWBIB26","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/0022-0000(78)90006-5","article-title":"T\u03c9 as a universal domain","volume":"17","author":"Plotkin","year":"1978","journal-title":"Journal of Computer and System Sciences"},{"key":"10.1016\/S1571-0661(04)00105-7_NEWBIB27","unstructured":"G.D. Plotkin. Full abstraction, totality and PCF. Accepted for publication, 1997."},{"year":"1967","series-title":"Theory of Recursive Functions and Effective Computability","author":"Rogers","key":"10.1016\/S1571-0661(04)00105-7_NEWBIB28"},{"key":"10.1016\/S1571-0661(04)00105-7_NEWBIB29","series-title":"Toposes, Algebraic Geometry and Logic","article-title":"continuous lattices","author":"Scot","year":"1972"},{"issue":"3","key":"10.1016\/S1571-0661(04)00105-7_NEWBIB30","doi-asserted-by":"crossref","first-page":"522","DOI":"10.1137\/0205037","article-title":"Data types as lattices","volume":"5","author":"Scott","year":"1976","journal-title":"SIAM Journal of Computing"},{"key":"10.1016\/S1571-0661(04)00105-7_NEWBIB31","doi-asserted-by":"crossref","unstructured":"D.S. Scott. A type-theoretical alternative to ISWIM, CU8CH, OWHY. Theoretical Computer Science, 121:411\u2013440, 1993. First written in 1969 and widely circulated in unpublished form since then.","DOI":"10.1016\/0304-3975(93)90095-B"},{"year":"1973","series-title":"Metamathematical Inverstigation of Intutionjistic Arithmetic and Analysis","author":"Troelstra","key":"10.1016\/S1571-0661(04)00105-7_NEWBIB32"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104001057?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104001057?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2024,12,15]],"date-time":"2024-12-15T09:13:49Z","timestamp":1734254029000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104001057"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"references-count":32,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1999]]}},"alternative-id":["S1571066104001057"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)00105-7","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[1999]]}}}