{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:21:56Z","timestamp":1776316916699,"version":"3.50.1"},"reference-count":72,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>\n                    Contextual equivalence is the\n                    <jats:italic toggle=\"yes\">de facto<\/jats:italic>\n                    standard notion of program equivalence. A key theorem is that contextual equivalence is an\n                    <jats:italic toggle=\"yes\">equational theory<\/jats:italic>\n                    . Making contextual equivalence more intensional, for example taking into account the time cost of the computation, seems a natural refinement. Such a change, however, does\n                    <jats:italic toggle=\"yes\">not<\/jats:italic>\n                    induce an equational theory, for an apparently essential reason: cost is not invariant under reduction.\n                  <\/jats:p>\n                  <jats:p>\n                    In the paradigmatic case of the untyped\n                    <jats:italic toggle=\"yes\">\u03bb<\/jats:italic>\n                    -calculus, we introduce\n                    <jats:italic toggle=\"yes\">interaction equivalence<\/jats:italic>\n                    . Inspired by game semantics, we observe the number of interaction steps between terms and contexts but\u2013crucially\u2013ignore their internal steps. We prove that interaction equivalence is an equational theory and characterize it as\n                    <jats:italic toggle=\"yes\">B<\/jats:italic>\n                    , the well-known theory induced by B\u00f6hm tree equality. It is the first observational characterization of\n                    <jats:italic toggle=\"yes\">B<\/jats:italic>\n                    obtained without enriching the discriminating power of contexts with extra features such as non-determinism. To prove our results, we develop interaction-based refinements of the B\u00f6hm-out technique and of intersection types.\n                  <\/jats:p>","DOI":"10.1145\/3704891","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1627-1656","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Interaction Equivalence"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4944-9944","authenticated-orcid":false,"given":"Beniamino","family":"Accattoli","sequence":"first","affiliation":[{"name":"Inria - Ecole Polytechnique, Palaiseau, France"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-5481-5719","authenticated-orcid":false,"given":"Adrienne","family":"Lancelot","sequence":"additional","affiliation":[{"name":"Inria - Ecole Polytechnique - Universit\u00e9 Paris Cit\u00e9, Palaiseau, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1448-9014","authenticated-orcid":false,"given":"Giulio","family":"Manzonetto","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris Cit\u00e9, Paris, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8762-8674","authenticated-orcid":false,"given":"Gabriele","family":"Vanoni","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris Cit\u00e9, Paris, France"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1006\/INCO.2000.2930"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1006\/INCO.1993.1044"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547650"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2303.08161"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679682000012X"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.FSCD.2024.23"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2409.18709"},{"key":"e_1_3_2_9_1","unstructured":"Peter Aczel. 1978. A General Church-Rosser Theorem. Technical Report. University of Manchester."},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17127-8_2"},{"key":"e_1_3_2_11_1","doi-asserted-by":"crossref","unstructured":"Henk Barendregt. 1977. The Type Free Lambda Calculus. In Handbook of Mathematical Logic Jon Barwise (Ed.). Studies in Logic and the Foundations of Mathematics Vol. 90. Elsevier 1091 \u2013 1132.","DOI":"10.1016\/S0049-237X(08)71129-7"},{"key":"e_1_3_2_12_1","volume-title":"The Lambda Calculus - Its Syntax and Semantics.","author":"Barendregt Henk","year":"1984","unstructured":"Henk Barendregt. 1984. The Lambda Calculus - Its Syntax and Semantics. Studies in logic and the foundations of mathematics, Vol.103. North-Holland."},{"key":"e_1_3_2_13_1","unstructured":"Henk Barendregt and Giulio Manzonetto. 2022. A Lambda Calculus Satellite. College Publications. https:\/\/www.collegepublications.co.uk\/logic\/mlf\/?00035"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19805-2_7"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17127-8_6"},{"key":"e_1_3_2_16_1","first-page":"1","article-title":"Alcune propriet\u00e0 delle forme \u03b2-\u03b7-normali nel","author":"B\u00f6hm Corrado","year":"1968","unstructured":"Corrado B\u00f6hm. 1968. Alcune propriet\u00e0 delle forme \u03b2-\u03b7-normali nel \u00c0.-K-calcolo. Pubblicazioni dell'istitutoper le applicazioni del calcolo 696 (1968), 1\u201319. Lavoro eseguito all'INAC.","journal-title":"\u00c0.-K-calcolo. Pubblicazioni dell'istitutoper le applicazioni del calcolo"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0037"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","unstructured":"Flavien Breuvart Giulio Manzonetto and Domenico Ruoppolo. 2018. Relational Graph Models at Work. Log. Methods Comput. Sci. 14 3 (2018). https:\/\/doi.org\/10.23638\/LMCS-14(3:2)2018 10.23638\/LMCS-14(3:2)2018","DOI":"10.23638\/LMCS-14(3:2)2018"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1093\/JIGPAL\/JZX018"},{"key":"e_1_3_2_20_1","unstructured":"Pierre Clairambault. 2024. Causal Investigations in Interactive Semantics. https:\/\/tel.archives-ouvertes.fr\/tel-04523273"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","unstructured":"Pierre Clairambault and Andrzej S. Murawski. 2013. B\u00f6hm Trees as Higher-Order Recursive Schemes. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science FST TCS 2013 December 12-14 2013 Guwahati India (LIPIcs Vol. 24) Anil Seth and Nisheeth K. Vishnoi (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik 91\u2013102. https:\/\/doi.org\/10.4230\/LIPICS.FSTTCS.2013.91 10.4230\/LIPICS.FSTTCS.2013.91","DOI":"10.4230\/LIPICS.FSTTCS.2013.91"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434313"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679682200003X"},{"key":"e_1_3_2_24_1","unstructured":"Daniel de Carvalho. 2007. S\u00e9mantiques de la logique lin\u00e9aire et temps de calcul. Th\u00e8se de Doctorat. Universit\u00e9 Aix-Marseille II."},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000396"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","unstructured":"Daniel de Carvalho Michele Pagani and Lorenzo Tortora de Falco. 2011. A semantic measure of the execution time in linear logic. Theor. Comput. Sci. 412 20 (2011) 1884\u20131902. https:\/\/doi.org\/10.1016\/J.TCS.2010.12.017 10.1016\/J.TCS.2010.12.017","DOI":"10.1016\/J.TCS.2010.12.017"},{"key":"e_1_3_2_27_1","unstructured":"Mariangiola Dezani-Ciancaglini. 2001. TLCA list Problem #18: Find trees representing contextual equivalences. See http:\/\/tlca.di.unito.it\/opltlca\/"},{"key":"e_1_3_2_28_1","first-page":"1","article-title":"B\u00f6hm's theorem for B\u00f6hm trees","volume":"98","author":"Dezani-Ciancaglini Mariangiola","year":"1998","unstructured":"Mariangiola Dezani-Ciancaglini, Benedetto Intrigila, and Marisa Venturini-Zilli. 1998. B\u00f6hm's theorem for B\u00f6hm trees. In ICTCS, Vol.98. World Scientific, 1\u201323.","journal-title":"ICTCS"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2773"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(2:4)2014"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129515000389"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632926"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040313"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CSL.2015.260"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/507635.507667"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628142"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.21"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236763"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0029520"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1112\/jlms\/s2-12.3.361"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","unstructured":"Martin Hyland Misao Nagayama John Power and Giuseppe Rosolini. 2004. A Category Theoretic Formulation for Engeler-style Models of the Untyped lambda. 161 (2004) 43\u201357. https:\/\/doi.org\/10.1016\/J.ENTCS.2006.04.024 10.1016\/J.ENTCS.2006.04.024","DOI":"10.1016\/J.ENTCS.2006.04.024"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1006\/INCO.2000.2917"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-15(1:6)2019"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2022.25"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371083"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00849-6"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394774"},{"key":"e_1_3_2_48_1","unstructured":"Jan Willem Klop. 1980. Combinatory Reduction Systems. PhD thesis. Utrecht University."},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480933"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73420-8_58"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.36"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","unstructured":"S\u00f8ren B. Lassen. 1999. Bisimulation in Untyped Lambda Calculus: B\u00f6hm Trees and Bisimulation up to Context. 20 (1999) 346\u2013374. https:\/\/doi.org\/10.1016\/S1571-0661(04)80083-5 10.1016\/S1571-0661(04)80083-5","DOI":"10.1016\/S1571-0661(04)80083-5"},{"key":"e_1_3_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603150"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292547"},{"key":"e_1_3_2_55_1","unstructured":"James Hiram Morris. 1968. Lambda-calculus Models of Programming Languages. Ph. D. Dissertation. Massachusetts Institute of Technology. https:\/\/books.google.is\/books?id=DklAAQAAIAAJ"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-97-2300-3_3"},{"key":"e_1_3_2_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1991.151658"},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS56636.2023.10175777"},{"key":"e_1_3_2_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.38"},{"key":"e_1_3_2_60_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005064"},{"key":"e_1_3_2_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45465-9_41"},{"key":"e_1_3_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3280984"},{"key":"e_1_3_2_63_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"e_1_3_2_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45099-3_19"},{"key":"e_1_3_2_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS56636.2023.10175686"},{"key":"e_1_3_2_66_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(96)00074-6"},{"key":"e_1_3_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/227699.227716"},{"key":"e_1_3_2_68_1","first-page":"275","volume-title":"Improvement theory and its applications","author":"Sands David","year":"1999","unstructured":"David Sands. 1999. Improvement theory and its applications. Cambridge University Press, USA, 275\u2013306."},{"key":"e_1_3_2_69_1","doi-asserted-by":"publisher","DOI":"10.1006\/INCO.1994.1042"},{"key":"e_1_3_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236950.3236952"},{"key":"e_1_3_2_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0073967"},{"key":"e_1_3_2_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04164-8_17"},{"key":"e_1_3_2_73_1","doi-asserted-by":"publisher","DOI":"10.1137\/0205036"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704891","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704891","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:15:18Z","timestamp":1770200118000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704891"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":72,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704891"],"URL":"https:\/\/doi.org\/10.1145\/3704891","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}