{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:12:03Z","timestamp":1775790723484,"version":"3.50.1"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2007,10,1]],"date-time":"2007-10-01T00:00:00Z","timestamp":1191196800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2007,10]]},"abstract":"<jats:p>\n            We present a bisimulation method for proving the contextual equivalence of packages in \u03bb-calculus with full existential and recursive types. Unlike traditional logical relations (either semantic or syntactic), our development is \u201celementary,\u201d using only sets and relations and avoiding advanced machinery such as domain theory, admissibility, and TT-closure. Unlike other bisimulations, ours is complete even for existential types. The key idea is to consider\n            <jats:italic>sets<\/jats:italic>\n            of relations\u2014instead of just relations\u2014as bisimulations.\n          <\/jats:p>","DOI":"10.1145\/1284320.1284325","type":"journal-article","created":{"date-parts":[[2007,10,19]],"date-time":"2007-10-19T16:11:36Z","timestamp":1192810296000},"page":"26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":45,"title":["A bisimulation for type abstraction and recursion"],"prefix":"10.1145","volume":"54","author":[{"given":"Eijiro","family":"Sumii","sequence":"first","affiliation":[{"name":"Tohoku University, Sendai, Japan"}]},{"given":"Benjamin C.","family":"Pierce","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, PA"}]}],"member":"320","published-online":{"date-parts":[[2007,10]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360213"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/640050.640052"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/266420.266432"},{"key":"e_1_2_1_4_1","volume-title":"Research Topics in Functional Programming","author":"Abramsky S.","unstructured":"Abramsky , S. 1990. The lazy lambda calculus . In Research Topics in Functional Programming , D. A. Turner, Ed. Addison-Wesley, Reading , MA , 65--117. Abramsky, S. 1990. The lazy lambda calculus. In Research Topics in Functional Programming, D. A. Turner, Ed. Addison-Wesley, Reading, MA, 65--117."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"e_1_2_1_6_1","unstructured":"Ahmed A. Appel A. W. and Virga R. 2003. An indexed model of impredicative polymorphism and mutable references. http:\/\/www.cs.princeton.edu\/~amal\/papers\/impred.pdf.  Ahmed A. Appel A. W. and Virga R. 2003. An indexed model of impredicative polymorphism and mutable references. http:\/\/www.cs.princeton.edu\/~amal\/papers\/impred.pdf."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science","volume":"2620","author":"Berger M.","unstructured":"Berger , M. , Honda , K. , and Yoshida , N . 2003. Genericity and the pi-calculus . In Proceedings of the Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science , vol. 2620 . Springer-Verlag, New York, 103--119. Berger, M., Honda, K., and Yoshida, N. 2003. Genericity and the pi-calculus. In Proceedings of the Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science, vol. 2620. Springer-Verlag, New York, 103--119."},{"key":"e_1_2_1_9_1","volume-title":"Higher Order Operational Techniques in Semantics. Electronic Notes in Theoretical Computer Science","volume":"41","author":"Bierman G. M.","unstructured":"Bierman , G. M. , Pitts , A. M. , and Russo , C. V . 2000. Operational properties of Lily, a polymorphic linear lambda calculus with recursion . In Higher Order Operational Techniques in Semantics. Electronic Notes in Theoretical Computer Science , vol. 41 . Elsevier Science, Amsterdam, The Netherlands. Bierman, G. M., Pitts, A. M., and Russo, C. V. 2000. Operational properties of Lily, a polymorphic linear lambda calculus with recursion. In Higher Order Operational Techniques in Semantics. Electronic Notes in Theoretical Computer Science, vol. 41. Elsevier Science, Amsterdam, The Netherlands."},{"key":"e_1_2_1_10_1","unstructured":"Birkedal L. and \n      Harper R\n  . \n  1999\n  . Relational interpretations of recursive types in an operational setting. Info. Comput. 155 1--2 3--63. (Summary appeared in Theoretical Aspects of Computer Software Lecture Notes in Computer Science vol. \n  1281 Springer-Verlag New York pp. \n  458\n  --\n  490 1997).   Birkedal L. and Harper R. 1999. Relational interpretations of recursive types in an operational setting. Info. Comput. 155 1--2 3--63. (Summary appeared in Theoretical Aspects of Computer Software Lecture Notes in Computer Science vol. 1281 Springer-Verlag New York pp. 458--490 1997)."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539700377864"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the 9th International Conference on Algebraic Methodology and Software Technology. Lecture Notes in Computer Science","volume":"2422","author":"Borgstr\u00f6m J.","unstructured":"Borgstr\u00f6m , J. , and Nestmann , U . 2002. On bisimulations for the spi calculus . In Proceedings of the 9th International Conference on Algebraic Methodology and Software Technology. Lecture Notes in Computer Science , vol. 2422 . Springer-Verlag, New York, 287--303. Borgstr\u00f6m, J., and Nestmann, U. 2002. On bisimulations for the spi calculus. In Proceedings of the 9th International Conference on Algebraic Methodology and Software Technology. Lecture Notes in Computer Science, vol. 2422. Springer-Verlag, New York, 287--303."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2829"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.010"},{"key":"e_1_2_1_15_1","unstructured":"Gordon A. D. 1995a. Bisimilarity as a theory of functional programming. mini-course. http:\/\/research.microsoft.com\/~adg\/Publications\/BRICS-NS-95-3.dvi.gz.  Gordon A. D. 1995a. Bisimilarity as a theory of functional programming. mini-course. http:\/\/research.microsoft.com\/~adg\/Publications\/BRICS-NS-95-3.dvi.gz."},{"key":"e_1_2_1_16_1","volume-title":"Higher Order Operational Techniques in Semantics","author":"Gordon A. D.","unstructured":"Gordon , A. D. 1995b. Operational equivalences for untyped and polymorphic object calculi . In Higher Order Operational Techniques in Semantics , Cambridge University Press , Cambridge, UK , 9--54. Gordon, A. D. 1995b. Operational equivalences for untyped and polymorphic object calculi. In Higher Order Operational Techniques in Semantics, Cambridge University Press, Cambridge, UK, 9--54."},{"key":"e_1_2_1_17_1","unstructured":"Gordon A. D. and Rees G. D. 1995. Bisimilarity for F&lt;:. Draft.  Gordon A. D. and Rees G. D. 1995. Bisimilarity for F &lt;: . Draft."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237807"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268976"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0008"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/788019.788861"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_11"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111050"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the 2007 International Workshop on Foundations and Developments of Object-Oriented Languages. http:\/\/foolwood07","author":"Koutavas V.","unstructured":"Koutavas , V. , and Wand , M . 2007. Reasoning about class behavior . In Proceedings of the 2007 International Workshop on Foundations and Developments of Object-Oriented Languages. http:\/\/foolwood07 .cs.uchicago.edu\/program\/koutavas.pdf. Koutavas, V., and Wand, M. 2007. Reasoning about class behavior. In Proceedings of the 2007 International Workshop on Foundations and Developments of Object-Oriented Languages. http:\/\/foolwood07.cs.uchicago.edu\/program\/koutavas.pdf."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.42"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73577"},{"key":"e_1_2_1_27_1","volume-title":"A Calculus of Communicating Systems. Number 92 in Lecture Notes in Computer Science","author":"Milner R.","unstructured":"Milner , R. 1980. A Calculus of Communicating Systems. Number 92 in Lecture Notes in Computer Science . Springer-Verlag , New York . Milner, R. 1980. A Calculus of Communicating Systems. Number 92 in Lecture Notes in Computer Science. Springer-Verlag, New York."},{"key":"e_1_2_1_28_1","volume-title":"Communication and Concurrency","author":"Milner R.","unstructured":"Milner , R. 1989. Communication and Concurrency . Prentice Hall, Englewood Cliffs , NJ. Milner, R. 1989. Communication and Concurrency. Prentice Hall, Englewood Cliffs, NJ."},{"key":"e_1_2_1_29_1","volume-title":"Communicating and Mobile Systems: The &pi;-Calculus","author":"Milner R.","unstructured":"Milner , R. 1999. Communicating and Mobile Systems: The &pi;-Calculus . Cambridge University Press , Cambridge, MA . Milner, R. 1999. Communicating and Mobile Systems: The &pi;-Calculus. Cambridge University Press, Cambridge, MA."},{"key":"e_1_2_1_30_1","volume-title":"Foundations for Programming Languages","author":"Mitchell J. C.","unstructured":"Mitchell , J. C. 1996. Foundations for Programming Languages . MIT Press , Cambridge, MA . Mitchell, J. C. 1996. Foundations for Programming Languages. MIT Press, Cambridge, MA."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/361932.361937"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/512927.512938"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/337244.337261"},{"key":"e_1_2_1_35_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/BFb0055063","volume-title":"Advanced Topics in Types and Programming Languages","author":"Pitts A.","year":"1998","unstructured":"Pitts , A. 2005. Typed operational reasoning . In Advanced Topics in Types and Programming Languages , B. C. Pierce, Ed. MIT Press, Cambridge, MA , Chapter 7, 245--289. (Preliminary version appeared as Existential Types : Logical Relations and Operational Equivalence in Automata, Languages and Programming, Lecture Notes in Computer Science , vol. 1443 , Springer-Verlag , pp. 309 -- 326 , 1998 ). Pitts, A. 2005. Typed operational reasoning. In Advanced Topics in Types and Programming Languages, B. C. Pierce, Ed. MIT Press, Cambridge, MA, Chapter 7, 245--289. (Preliminary version appeared as Existential Types: Logical Relations and Operational Equivalence in Automata, Languages and Programming, Lecture Notes in Computer Science, vol. 1443, Springer-Verlag, pp. 309--326, 1998)."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500003066"},{"key":"e_1_2_1_37_1","volume-title":"Lecture Notes in Computer Science","volume":"711","author":"Pitts A. M.","unstructured":"Pitts , A. M. , and Stark , I . 1993. Observable properties of higher order functions that dynamically create local names, or: What's new&quest; In Proceedings of the Symposium on Mathematical Foundations of Computer Science . Lecture Notes in Computer Science , vol. 711 . Springer-Verlag, New York, 122--141. Pitts, A. M., and Stark, I. 1993. Observable properties of higher order functions that dynamically create local names, or: What's new&quest; In Proceedings of the Symposium on Mathematical Foundations of Computer Science. Lecture Notes in Computer Science, vol. 711. Springer-Verlag, New York, 122--141."},{"key":"e_1_2_1_38_1","unstructured":"Pitts A. M. and Stark I. 1998. Operational reasoning for functions with local state. In Higher Order Operational Techniques in Semantics. Cambridge University Press Cambridge MA 227--273.   Pitts A. M. and Stark I. 1998. Operational reasoning for functions with local state. In Higher Order Operational Techniques in Semantics. Cambridge University Press Cambridge MA 227--273."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.17"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964015"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1284320.1284325","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1284320.1284325","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T15:14:01Z","timestamp":1750259641000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1284320.1284325"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,10]]},"references-count":41,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2007,10]]}},"alternative-id":["10.1145\/1284320.1284325"],"URL":"https:\/\/doi.org\/10.1145\/1284320.1284325","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,10]]},"assertion":[{"value":"2007-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}