{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:24:20Z","timestamp":1761611060267},"reference-count":42,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[2002,3,1]],"date-time":"2002-03-01T00:00:00Z","timestamp":1014940800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4156,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2002,3]]},"DOI":"10.1016\/s0304-3975(00)00309-1","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T11:09:53Z","timestamp":1027595393000},"page":"183-230","source":"Crossref","is-referenced-by-count":38,"title":["From rewrite rules to bisimulation congruences"],"prefix":"10.1016","volume":"274","author":[{"given":"Peter","family":"Sewell","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(00)00309-1_BIB1","doi-asserted-by":"crossref","unstructured":"M. Abadi, A.D. Gordon, A calculus for cryptographic protocols: the spi calculus, in: Proc. 4th ACM Conf. on Computer and Communications Security, Z\u00fcrich, ACM Press, New York, April 1997, pp. 36\u201347.","DOI":"10.1145\/266420.266432"},{"key":"10.1016\/S0304-3975(00)00309-1_BIB2","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":"Inform. and Comput."},{"issue":"1","key":"10.1016\/S0304-3975(00)00309-1_BIB3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1040","article-title":"Turning SOS rules into equations","volume":"111","author":"Aceto","year":"1994","journal-title":"Inform. and Comput."},{"year":"1998","series-title":"Term Rewriting and All That","author":"Baader","key":"10.1016\/S0304-3975(00)00309-1_BIB4"},{"key":"10.1016\/S0304-3975(00)00309-1_BIB5","unstructured":"J.-P. Ban\u00e2tre, D. Le M\u00e9tayer, A new computational model and its discipline of programming, Technical Report No. 566, INRIA, 1986."},{"key":"10.1016\/S0304-3975(00)00309-1_BIB6","doi-asserted-by":"crossref","unstructured":"K.L. Bernstein, A congruence theorem for structured operational semantics of higher-order languages, in: Proc. LICS 98, 1998.","DOI":"10.1109\/LICS.1998.705652"},{"key":"10.1016\/S0304-3975(00)00309-1_BIB7","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0304-3975(92)90185-I","article-title":"The chemical abstract machine","volume":"96","author":"Berry","year":"1992","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"10.1016\/S0304-3975(00)00309-1_BIB8","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1145\/200836.200876","article-title":"Bisimulation can't be traced","volume":"42","author":"Bloom","year":"1995","journal-title":"J. ACM"},{"key":"10.1016\/S0304-3975(00)00309-1_BIB9","doi-asserted-by":"crossref","unstructured":"G. Boudol, The \u03c0-calculus in direct style, Proc. 24th POPL, 15\u201317 January 1997, pp. 228\u2013241.","DOI":"10.1145\/263699.263726"},{"key":"10.1016\/S0304-3975(00)00309-1_BIB10","doi-asserted-by":"crossref","unstructured":"L. Cardelli, A.D. Gordon, Mobile ambients, in: Proc. Foundations of Software Science and Computation Structures, FoSSaCS, ETAPS\u201998, Lecture Notes in Computer Science, vol. 1378, Springer, Berlin, March 1998, pp. 140\u2013155.","DOI":"10.1007\/BFb0053547"},{"key":"10.1016\/S0304-3975(00)00309-1_BIB11","doi-asserted-by":"crossref","unstructured":"G.L. Cattani, A.J. Power, G. Winskel, A categorical axiomatics for bisimulation, in: Proc. CONCUR \u201998: Concurrency Theory, Nice, Lecture Notes in Computer Science, vol. 1466, Springer, Berlin, September 1998.","DOI":"10.1007\/BFb0055649"},{"key":"10.1016\/S0304-3975(00)00309-1_BIB12","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/0304-3975(84)90113-0","article-title":"Testing equivalences for processes","volume":"34","author":"De Nicola","year":"1984","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00309-1_BIB13","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1016\/0304-3975(85)90093-3","article-title":"Higher-level synchronising devices in MEIJE\u2013SCCS","volume":"37","author":"de Simone","year":"1985","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00309-1_BIB14","doi-asserted-by":"crossref","unstructured":"U. Engberg, M. Nielsen, A calculus of communicating systems with label-passing. Technical Report DAIMI PB-208, Computer Science Department, University of Aarhus, Denmark, 1986.","DOI":"10.7146\/dpb.v15i208.7559"},{"key":"10.1016\/S0304-3975(00)00309-1_BIB15","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\/S0304-3975(00)00309-1_BIB16","doi-asserted-by":"crossref","unstructured":"W. Ferreira, M. Hennessy, A. Jeffrey, A theory of weak bisimulation for core CML, in: Proc. ACM SIGPLAN Internat. Conf. Functional Programming, ACM Press, New York, 1996.","DOI":"10.1145\/232627.232649"},{"key":"10.1016\/S0304-3975(00)00309-1_BIB17","doi-asserted-by":"crossref","unstructured":"C. Fournet, G. Gonthier, The reflexive CHAM and the join-calculus, in: Proc. 23rd POPL, ACM Press, New York, January 1996, pp. 372\u2013385.","DOI":"10.1145\/237721.237805"},{"key":"10.1016\/S0304-3975(00)00309-1_BIB18","unstructured":"F. Gadducci, U. Montanari, The tile model, in: G. Plotkin, C. Stirling, M. Tofte (Eds.), Proof, Language and Interaction: Essays in Honour of Robin Milner, MIT Press, Cambridge, MA, 2000."},{"key":"10.1016\/S0304-3975(00)00309-1_BIB19","first-page":"278","article-title":"The linear time \u2013 branching time spectrum","volume":"vol. 458","author":"van Glabbeek","year":"1990"},{"key":"10.1016\/S0304-3975(00)00309-1_BIB20","first-page":"66","article-title":"The linear time \u2013 branching time spectrum II; the semantics of sequential systems with silent moves","volume":"vol. 715","author":"van Glabbeek","year":"1993"},{"key":"10.1016\/S0304-3975(00)00309-1_BIB21","unstructured":"A.D. Gordon, Bisimilarity as a theory of functional programming. mini-course, Number NS-95-3 in the BRICS Notes Series, Computer Science Department, Aarhus, 1995."},{"key":"10.1016\/S0304-3975(00)00309-1_BIB22","doi-asserted-by":"crossref","unstructured":"A.D. Gordon, G.D. Rees, Bisimilarity for a first-order calculus of objects with subtyping, Proceedings of the 23rd POPL, 1996, pp. 386\u2013395.","DOI":"10.1145\/237721.237807"},{"issue":"2","key":"10.1016\/S0304-3975(00)00309-1_BIB23","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1016\/0890-5401(92)90013-6","article-title":"Structured operational semantics and bisimulation as a congruence","volume":"100","author":"Groote","year":"1992","journal-title":"Inform. Comput."},{"issue":"2","key":"10.1016\/S0304-3975(00)00309-1_BIB24","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1016\/0304-3975(95)00074-7","article-title":"On reduction-based process semantics","volume":"152","author":"Honda","year":"1995","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00309-1_BIB25","doi-asserted-by":"crossref","unstructured":"D.J. Howe, Equality in lazy computation systems, Proc. LICS \u201989, 1989, pp. 193\u2013203.","DOI":"10.1109\/LICS.1989.39174"},{"key":"10.1016\/S0304-3975(00)00309-1_BIB26","unstructured":"A. Mifsud, Control Structures, Ph.D. Thesis, University of Edinburgh, 1996."},{"issue":"1","key":"10.1016\/S0304-3975(00)00309-1_BIB27","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","article-title":"A calculus of mobile processes, Parts I + II","volume":"100","author":"Milner","year":"1992","journal-title":"Inform. and Comput."},{"issue":"2","key":"10.1016\/S0304-3975(00)00309-1_BIB28","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1017\/S0960129500001407","article-title":"Functions as processes","volume":"2","author":"Milner","year":"1992","journal-title":"J. Math. Struct. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00309-1_BIB29","doi-asserted-by":"crossref","first-page":"707","DOI":"10.1007\/s002360050067","article-title":"Calculi for interaction","volume":"33","author":"Milner","year":"1996","journal-title":"Acta Inform."},{"key":"10.1016\/S0304-3975(00)00309-1_BIB30","first-page":"685","article-title":"Barbed bisimulation","volume":"vol. 623","author":"Milner","year":"1992"},{"key":"10.1016\/S0304-3975(00)00309-1_BIB31","first-page":"171","article-title":"Dynamic congruence vs. progressing bisimulation for CCS","volume":"XVI","author":"Montanari","year":"1992","journal-title":"Fund. Inform."},{"key":"10.1016\/S0304-3975(00)00309-1_BIB32","first-page":"171","article-title":"Constraints for free in concurrent computation","volume":"vol. 1023","author":"Niehren","year":"1995"},{"key":"10.1016\/S0304-3975(00)00309-1_BIB33","unstructured":"G.D. Plotkin, A structural approach to operational semantics, Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark, 1981."},{"key":"10.1016\/S0304-3975(00)00309-1_BIB34","doi-asserted-by":"crossref","unstructured":"J. Riely, M. Hennessy, A typed language for distributed mobile processes, Proc. 25th POPL, January 1998.","DOI":"10.1145\/268946.268978"},{"key":"10.1016\/S0304-3975(00)00309-1_BIB35","unstructured":"D. Sangiorgi, Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms, Ph.D. Thesis, University of Edinburgh, 1993."},{"key":"10.1016\/S0304-3975(00)00309-1_BIB36","first-page":"391","article-title":"On implementations and semantics of a concurrent programming language","volume":"vol. 1243","author":"Sewell","year":"1997"},{"key":"10.1016\/S0304-3975(00)00309-1_BIB37","unstructured":"P. Sewell, From rewrite rules to bisimulation congruences, Technical Report No. 444, University of Cambridge, June 1998. Available from http:\/\/www.cl.cam.ac.uk\/users\/pes20\/."},{"key":"10.1016\/S0304-3975(00)00309-1_BIB38","unstructured":"P. Sewell, From rewrite rules to bisimulation congruences, in: Proc. CONCUR \u201998: Concurrency Theory, Nice, Lecture Notes in Computer Science, vol. 1466, Springer, Berlin, September 1998, pp. 269\u2013284."},{"key":"10.1016\/S0304-3975(00)00309-1_BIB39","first-page":"695","article-title":"Global\/local subtyping and capability inference for a distributed \u03c0-calculus","volume":"vol. 1443","author":"Sewell","year":"1998"},{"key":"10.1016\/S0304-3975(00)00309-1_BIB40","doi-asserted-by":"crossref","unstructured":"A. Rensink, Bisimilarity of open terms, in: Expressiveness in Concurrency, 1997. Full report version: Hildesheimer Informatik-Bericht 5\/97, University of Hildesheim, May 1997.","DOI":"10.1016\/S1571-0661(05)80477-3"},{"key":"10.1016\/S0304-3975(00)00309-1_BIB41","first-page":"280","article-title":"Towards a mathematical operational semantics","author":"Turi","year":"1997"},{"key":"10.1016\/S0304-3975(00)00309-1_BIB42","unstructured":"F. van Raamsdonk, Confluence and normalisation for higher-order rewriting, Ph.D. Thesis, Vrije Universiteit, Amsterdam, 1996."}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397500003091?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397500003091?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T05:15:04Z","timestamp":1578460504000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397500003091"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,3]]},"references-count":42,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2002,3]]}},"alternative-id":["S0304397500003091"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(00)00309-1","relation":{},"ISSN":["0304-3975"],"issn-type":[{"type":"print","value":"0304-3975"}],"subject":[],"published":{"date-parts":[[2002,3]]}}}