{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:21:53Z","timestamp":1776316913690,"version":"3.50.1"},"reference-count":23,"publisher":"Elsevier BV","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)80083-5","type":"journal-article","created":{"date-parts":[[2004,12,13]],"date-time":"2004-12-13T17:55:14Z","timestamp":1102960514000},"page":"346-374","source":"Crossref","is-referenced-by-count":26,"special_numbering":"C","title":["Bisimulation in Untyped Lambda Calculus:"],"prefix":"10.1016","volume":"20","author":[{"given":"S.B.","family":"Lassen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80083-5_NEWBIB1","series-title":"Research Topics in Functional Programming","first-page":"65","article-title":"The lazy lambda calculus","author":"Abramsky","year":"1990"},{"key":"10.1016\/S1571-0661(04)80083-5_NEWBIB2","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1006\/inco.1993.1044","article-title":"Full abstraction in the lazy lambda calculus","volume":"105","author":"Abramsky","year":"1993","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(04)80083-5_NEWBIB3","series-title":"Number 103 in Studies in Logic and the Foundations of Mathematics","doi-asserted-by":"crossref","DOI":"10.1016\/S0049-237X(08)71818-4","article-title":"The Lambda Calculus: Its Syntax and Semantics","author":"Barendregt","year":"1984"},{"key":"10.1016\/S1571-0661(04)80083-5_NEWBIB4","unstructured":"G. Berry, \u201cMod\u00e8les compl\u00e8tement ad\u00e9quats et stables des lambda calculus typ\u00e9s,\u201d Th\u00e8se de doctorat d'etat, Universit\u00e9 Paris VII, 1979."},{"key":"10.1016\/S1571-0661(04)80083-5_NEWBIB5","unstructured":"G. Boudol, On the semantics of the call-by-name CPS transform, Theoretical Computer Science, 1999, Note, To appear."},{"key":"10.1016\/S1571-0661(04)80083-5_NEWBIB6","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1016\/S0304-3975(97)00004-2","article-title":"A syntactical proof of the operational equivalence of two \u03bb-terms","volume":"180","author":"David","year":"1997","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80083-5_NEWBIB7","doi-asserted-by":"crossref","unstructured":"M. Dezani-Ciancaglini, J. Tiuryn, and P. Urzyczyn, Discrimination by parallel observers, In: Proc. 12th Annual IEEE Symposium on Logic in Computer Science, 1997, pages 396\u2013407.","DOI":"10.1109\/LICS.1997.614965"},{"key":"10.1016\/S1571-0661(04)80083-5_NEWBIB8","doi-asserted-by":"crossref","unstructured":"H. Goguen, Soundness of typed operational semantics for the logical framework, In: Proc. 4th International Conference on Typed Lambda Calculus and Applications, L'Aquila, Italy, Lecture Notes in Computer Science 1581 (1999), Springer-Verlag.","DOI":"10.1007\/3-540-48959-2_14"},{"key":"10.1016\/S1571-0661(04)80083-5_NEWBIB9","doi-asserted-by":"crossref","unstructured":"A. D. Gordon, Bisimilarity as a theory of functional programming, In: Proc. 11th Conference of Mathematical Foundations of Programming Semantics, Electronic Notes in Theoretical Computer Science 1 (1995), URL: http:\/\/www.elsevier.nl\/locate\/entcs\/volume1.html.","DOI":"10.1016\/S1571-0661(04)80013-6"},{"key":"10.1016\/S1571-0661(04)80083-5_NEWBIB10","series-title":"Higher Order operational Techniques in Semantics","year":"1998"},{"key":"10.1016\/S1571-0661(04)80083-5_NEWBIB11","unstructured":"F. Honsell and M. Lenisa, Final semantics for untyped lambda-calculus, In: Proc. 2nd International Conference on Typed Lambda Calculus and Applications, Edinburgh, Lecture Notes in Computer Science 902 (1995), pp. 249\u2013265."},{"key":"10.1016\/S1571-0661(04)80083-5_NEWBIB12","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1006\/inco.1996.0008","article-title":"Proving congruence of bisimulation in functional programming languages","volume":"124","author":"Howe","year":"1996","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(04)80083-5_NEWBIB13","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1112\/jlms\/s2-12.3.361","article-title":"A Syntactic characterisation of the equality in some models for the lambda calculus","volume":"12","author":"Hyland","year":"1976","journal-title":"Journal of the London Mathematical Society"},{"key":"10.1016\/S1571-0661(04)80083-5_NEWBIB14","first-page":"222","article-title":"A tutorial on (co)algebras and (co)induction","volume":"62","author":"Jacobs","year":"1997","journal-title":"Bulletin of the EATCS"},{"key":"10.1016\/S1571-0661(04)80083-5_NEWBIB15","doi-asserted-by":"crossref","unstructured":"S. B. Lassen, Relational reasoning about contexts, In: Gordon and Pitts [10], pages 91\u2013135.","DOI":"10.7146\/brics.v4i24.18950"},{"key":"10.1016\/S1571-0661(04)80083-5_NEWBIB16","doi-asserted-by":"crossref","unstructured":"M. Lenisa, A uniform syntactical method for proving coinduction principles in \u03bb-calculi, In: M. Bidoit and M. Dauchet, editors, TAPSOFT '97, Lecture Notes in Computer Science 1214 (1997), pp. 309\u2013320.","DOI":"10.1007\/BFb0030606"},{"key":"10.1016\/S1571-0661(04)80083-5_NEWBIB17","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1016\/0168-0072(83)90030-1","article-title":"Set-theoretical models of lambda calculus: Theories, expansions and isomophisms","volume":"24","author":"Longo","year":"1983","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.1016\/S1571-0661(04)80083-5_NEWBIB18","unstructured":"J. H. Morris, \u201cLambda-Calculus Models of Programming Languages,\u201d PhD thesis, MIT, Dec. 1968."},{"key":"10.1016\/S1571-0661(04)80083-5_NEWBIB19","unstructured":"C.-H. L. Ong, \u201cThe Lazy Lambda Calculus: An Investigation into the Foundations of Functional Programming,\u201d PhD thesis, University of London, 1988."},{"key":"10.1016\/S1571-0661(04)80083-5_NEWBIB20","unstructured":"D. Sands, Improvement theory and its applications, In Gordon and Pitts [10], pages 275\u2013306."},{"key":"10.1016\/S1571-0661(04)80083-5_NEWBIB21","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1006\/inco.1994.1042","article-title":"The lazy lambda calculus in a concurrency senario","volume":"111","author":"Sangiorgi","year":"1994","journal-title":"Information and Computation"},{"key":"10.1016\/S1571-0661(04)80083-5_NEWBIB22","unstructured":"D. Sangiorgi, On the bisimulation proof method, Technical Report LFCS-94-299, University of Edinburgh, Aug. 1994."},{"key":"10.1016\/S1571-0661(04)80083-5_NEWBIB23","doi-asserted-by":"crossref","first-page":"488","DOI":"10.1137\/0205036","article-title":"The relation between computational and denotational properties for Scott's D\u221e-models of the lambda-calculus","volume":"5","author":"Wadsworth","year":"1976","journal-title":"SIAM Journal on Computing"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104800835?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104800835?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T17:45:28Z","timestamp":1586022328000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104800835"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"references-count":23,"alternative-id":["S1571066104800835"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80083-5","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]}}}