{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T03:30:58Z","timestamp":1778297458875,"version":"3.51.4"},"reference-count":31,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":6784,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[1995]]},"DOI":"10.1016\/s1571-0661(04)80013-6","type":"journal-article","created":{"date-parts":[[2004,9,28]],"date-time":"2004-09-28T15:29:25Z","timestamp":1096385365000},"page":"232-252","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":41,"special_numbering":"C","title":["Bisimilarity as a Theory of Functional Programming"],"prefix":"10.1016","volume":"1","author":[{"given":"Andrew D.","family":"Gordon","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB1","unstructured":"Samson Abramsky. The lazy lambda calculus. In Turner [29], pages 65\u2013116."},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB2","series-title":"Handbook of Mathematical Logic","first-page":"739","article-title":"An introduction to inductive definitions","author":"Aczel","year":"1977"},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB3","doi-asserted-by":"crossref","unstructured":"Karen L. Bernstein and Eugene W. Stark. Operational semantics of a focusing debugger. In Eleventh Annual Conference on Mathematical Foundations of Programming Semantics, volume 1 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers B.V., 1995.","DOI":"10.1016\/S1571-0661(04)80002-1"},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB4","doi-asserted-by":"crossref","unstructured":"Bard Bloom. Can LCF be topped? Flat lattice models of typed lambda calculus. In Proceedings of the 3rd IEEE Symposium on Logic in Computer Science, pages 282\u2013295. IEEE Computer Society Press, 1988.","DOI":"10.1109\/LICS.1988.5127"},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB5","doi-asserted-by":"crossref","unstructured":"Thierry Coquand. Infinite objects in type theory. In Types of Proofs and Programs, pages 62\u201378, volume 806 of Lecture Notes in Computer Science. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-58085-9_72"},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB6","doi-asserted-by":"crossref","unstructured":"Roy L. Crole and Andrew D. Gordon. A sound metalogical semantics for input\/output effects. In Computer Science Logic'94, Kazimierz, Poland, September 1994, volume 933 of Lecture Notes in Computer Science. Springer-Verlag, June 1995.","DOI":"10.1007\/BFb0022267"},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB7","series-title":"Introduction to Lattices and Order","author":"Davey","year":"1990"},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB8","series-title":"Formal Description of Programming Concepts III","first-page":"193","article-title":"Control operators, the SECD-machine, and the \u03bb-calculus","author":"Felleisen","year":"1986"},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB9","series-title":"Functional Programming and Input\/Output","author":"Andrew Gordon","year":"1994"},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB10","series-title":"Semantics of Programming Languages: Structures and Techniques","author":"Carl Gunter","year":"1992"},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB11","unstructured":"Douglas J. Howe. Equality in lazy computation systems. In Proceedings of the 4th IEEE Symposium on Logic in Computer Science, pages 198\u2013203, 1989."},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB12","unstructured":"Douglas J. Howe. Proving congruence of bisimulation in functional programming languages. Preprint, 1994."},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB13","unstructured":"I. A. Mason, S. F. Smith, and C. L. Talcott. From operational semantics to domain theory. Submitted for publication, 1994."},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB14","doi-asserted-by":"crossref","unstructured":"Thomas F. Melham. A package for inductive relation definitions in HOL. In Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, Davis, California, pages 350\u2013357. IEEE Computer Society Press, 1991.","DOI":"10.1109\/HOL.1991.596299"},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB15","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(77)90053-6","article-title":"Fully abstract models of typed lambda-calculi","volume":"4","author":"Milner","year":"1977","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB16","series-title":"Communication and Concurrency","author":"Milner","year":"1989"},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB17","unstructured":"James H. Morris. Lambda-Calculus Models of Programming Languages. PhD thesis, MIT, December 1968."},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB18","unstructured":"C.-H. Luke Ong. Correspondence between operational and denotational semantics: The full abstraction problem for PCF. Submitted to Handbook of Logic in Computer Science Volume 3, OUP 1994, January 1994."},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB19","doi-asserted-by":"crossref","unstructured":"David Park. Concurrency and automata on infinite sequences. In Peter Deussen, editor, Theoretical Computer Science: 5th GI-Conference, Karlsruhe, volume 104 of Lecture Notes in Computer Science, pages 167\u2013183. Springer-Verlag, March 1981.","DOI":"10.1007\/BFb0017309"},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB20","unstructured":"Lawrence C. Paulson. Co-induction and co-recursion in higher-order logic. Technical Report 304, University of Cambridge Computer Laboratory, 1993."},{"issue":"8","key":"10.1016\/S1571-0661(04)80013-6_NEWBIB21","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1145\/47907.47910","article-title":"FLIC\u2013a functional language intermediate code","volume":"23","author":"Simon Peyton","year":"1988","journal-title":"ACM SIGPLAN Notices"},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB22","doi-asserted-by":"crossref","unstructured":"Andrew Pitts and Ian Stark. On the observable properties of higher order functions that dynamically create local names (preliminary report). In SIPL'93:ACM SIGPLAN Workshop on State in Programming Languages, pages 31\u201345, June 1993.","DOI":"10.1007\/3-540-57182-5_8"},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB23","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1016\/0304-3975(94)90014-0","article-title":"A co-induction principle for recursively defined domains","volume":"124","author":"Andrew Pitts","year":"1994","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB24","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":"Gordon Plotkin","year":"1977","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB25","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1017\/S0960129500000293","article-title":"Fully abstract translations between functional languages","volume":"3","author":"Jon Riecke","year":"1993","journal-title":"Mathematical Structures in Computer Science"},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB26","doi-asserted-by":"crossref","unstructured":"Eike Ritter and Andrew M. Pitts. A fully abstract translation between a \u03bb-calculus with reference types and Standard ML. In Proceedings TLCA '95, Edinburgh, 1995.","DOI":"10.1007\/BFb0014067"},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB27","series-title":"Functional Programming, Glasgow 1991, Workshops in Computing","first-page":"298","article-title":"Operational theories of improvement in functional languages (extended abstract)","author":"Sands","year":"1992"},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB28","unstructured":"Davide Sangiorgi. On the bisimulation proof method. Technical Report ECS\u2013LFCS\u201394\u2013299, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, August 1994."},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB29","series-title":"Research Topics in Functional Programming","author":"Turner","year":"1990"},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB30","doi-asserted-by":"crossref","first-page":"461","DOI":"10.1017\/S0960129500001560","article-title":"Comprehending monads","volume":"2","author":"Wadler","year":"1992","journal-title":"Mathematical Structures in Computer Science"},{"key":"10.1016\/S1571-0661(04)80013-6_NEWBIB31","series-title":"The Formal Semantics of Programming Languages","author":"Winskel","year":"1993"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104800136?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104800136?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:03:26Z","timestamp":1761609806000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104800136"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"references-count":31,"alternative-id":["S1571066104800136"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80013-6","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[1995]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Bisimilarity as a Theory of Functional Programming","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(04)80013-6","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2000 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}