{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T14:33:16Z","timestamp":1787063596225,"version":"3.56.0"},"reference-count":78,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T00:00:00Z","timestamp":1609718400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["GA 818616"],"award-info":[{"award-number":["GA 818616"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-16-CE40-004-01"],"award-info":[{"award-number":["ANR-16-CE40-004-01"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,1,4]]},"abstract":"<jats:p>\n                    Evaluating higher-order functional programs through abstract machines inspired by the geometry of the interaction is known to induce\n                    <jats:italic toggle=\"yes\">space<\/jats:italic>\n                    efficiencies, the price being\n                    <jats:italic toggle=\"yes\">time<\/jats:italic>\n                    performances often poorer than those obtainable with traditional, environment-based, abstract machines. Although families of lambda-terms for which the former is exponentially less efficient than the latter do exist, it is currently unknown how\n                    <jats:italic toggle=\"yes\">general<\/jats:italic>\n                    this phenomenon is, and how far the inefficiencies can go, in the worst case. We answer these questions formulating four different well-known abstract machines inside a common definitional framework, this way being able to give sharp results about the relative time efficiencies. We also prove that non-idempotent intersection type theories are able to precisely reflect the time performances of the interactive abstract machine, this way showing that its time-inefficiency ultimately descends from the presence of higher-order types.\n                  <\/jats:p>","DOI":"10.1145\/3434332","type":"journal-article","created":{"date-parts":[[2021,1,4]],"date-time":"2021-01-04T12:34:24Z","timestamp":1609763664000},"page":"1-33","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["The (In)Efficiency of interaction"],"prefix":"10.1145","volume":"5","author":[{"given":"Beniamino","family":"Accattoli","sequence":"first","affiliation":[{"name":"Inria, France \/ \u00c9cole Polytechnique, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9200-070X","authenticated-orcid":false,"given":"Ugo","family":"Dal Lago","sequence":"additional","affiliation":[{"name":"University of Bologna, Italy \/ Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gabriele","family":"Vanoni","sequence":"additional","affiliation":[{"name":"University of Bologna, Italy \/ Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,1,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628154"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3131851.3131855"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3354166.3354169"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.RTA"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","unstructured":"Beniamino Accattoli and Ugo Dal Lago. 2016. (Leftmost-Outermost) Beta Reduction is Invariant Indeed. Logical Methods in Computer Science 12 1 ( 2016 ). https:\/\/doi.org\/10.2168\/LMCS-12 ( 1 :4) 2016 10.2168\/LMCS-12(1:4)2016","DOI":"10.2168\/LMCS-12"},{"key":"e_1_2_1_8_1","unstructured":"Beniamino Accattoli Ugo Dal Lago and Gabriele Vanoni. 2020a. The (In)Eficiency of Interaction. Technical Report. https:\/\/arxiv.org\/abs\/ 2010.12988."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3414080.3414108"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","unstructured":"Beniamino Accattoli St\u00e9phane Graham-Lengrand and Delia Kesner. 2020c. Tight typings and split bounds fully developed. J. Funct. Program. 30 ( 2020 ) e14. https:\/\/doi.org\/10.1017\/S095679682000012X 10.1017\/S095679682000012X","DOI":"10.1017\/S095679682000012X"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02768-1_3"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_15"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/jsl"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS"},{"key":"e_1_2_1_16_1","unstructured":"Patrick Baillot. 1999. Approches dynamiques en s\u00e9mantique de la logique lineaire: jeux et g\u00e9om\u00e9trie de l'interaction. PhD Thesis. Universite Aix-Marseille 2."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic"},{"key":"e_1_2_1_18_1","unstructured":"Hendrik Pieter Barendregt. 1984. The lambda calculus: its syntax and semantics. North-Holland."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018882.3020004"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","unstructured":"Alexis Bernadet and St\u00e9phane Graham-Lengrand. 2013. Non-idempotent intersection types and strong normalisation. Logical Methods in Computer Science 9 4 ( 2013 ). https:\/\/doi.org\/10.2168\/LMCS-9( 4 :3) 2013 10.2168\/LMCS-9(4:3)2013","DOI":"10.2168\/LMCS-9("},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224210"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.08.035"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59025-3_2"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzx018"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19805-2_23"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","unstructured":"Pierre Clairambault. 2015. Bounding linear head reduction and visible interaction through skeletons. Log. Methods Comput. Sci. 11 2 ( 2015 ). https:\/\/doi.org\/10.2168\/LMCS-11 ( 2 :6) 2015 10.2168\/LMCS-11(2:6)2015","DOI":"10.2168\/LMCS-11"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","unstructured":"Mario Coppo and Mariangiola Dezani-Ciancaglini. 1978. A new type assignment for \u03bb-terms. Arch. Math. Log. 19 1 ( 1978 ) 139-156. https:\/\/doi.org\/10.1007\/BF02011875 10.1007\/BF02011875","DOI":"10.1007\/BF02011875"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093883253"},{"key":"e_1_2_1_29_1","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism","author":"Coppo Mario","unstructured":"Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. 1980. Principal Type Schemes and Lambda-calculus Semantics. In To H.B. Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism. Academic Press, 535-560. http:\/\/www.di.unito.it\/~dezani\/papers\/CDV80.pdf"},{"key":"e_1_2_1_30_1","volume-title":"Computing with Abstract B\u00f6hm Trees. In Third Fuji International Symposium on Functional and Logic Programming, FLOPS 1998","author":"Curien Pierre-Louis","year":"1998","unstructured":"Pierre-Louis Curien and Hugo Herbelin. 1998. Computing with Abstract B\u00f6hm Trees. In Third Fuji International Symposium on Functional and Logic Programming, FLOPS 1998, Kyoto, Japan, Apil 2-4, 1998, Masahiko Sato and Yoshihito Toyama (Eds.). World Scientific, Singapore, 20-39."},{"key":"e_1_2_1_31_1","unstructured":"Pierre-Louis Curien and Hugo Herbelin. 2007. Abstract machines for dialogue games. ( 2007 ). http:\/\/arxiv.org\/abs\/0706.2544"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603154"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_12"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.176.6"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.5555\/212876.212903"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","unstructured":"Vincent Danos and Laurent Regnier. 1999. Reversible irreversible and optimal lambda-machines. Theoretical Computer Science 227 1 ( 1999 ) 79-97. https:\/\/doi.org\/10.1016\/S0304-3975 ( 99 ) 00049-3 10.1016\/S0304-3975(99)00049-3","DOI":"10.1016\/S0304-3975"},{"key":"e_1_2_1_42_1","unstructured":"Vincent Danos and Laurent Regnier. 2004. Head Linear Reduction. Technical Report."},{"key":"e_1_2_1_43_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_2_1_44_1","doi-asserted-by":"publisher","unstructured":"Daniel de Carvalho. 2018. Execution time of \u03bb-terms via denotational semantics and intersection types. Math. Str. in Comput. Sci. 28 7 ( 2018 ) 1169-1203. https:\/\/doi.org\/10.1017\/S0960129516000396 10.1017\/S0960129516000396","DOI":"10.1017\/S0960129516000396"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45832-8_8"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57887-0_115"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190269"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","unstructured":"Jean-Yves Girard. 1987. Linear logic. Theoretical Computer Science 50 1 ( 1987 ) 1-101. https:\/\/doi.org\/10.1016\/ 0304-3975 ( 87 ) 90045-4 10.1016\/0304-3975(87)90045-4","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_1_51_1","volume-title":"Studies in Logic and the Foundations of Mathematics","author":"Girard Jean-Yves","unstructured":"Jean-Yves Girard. 1989. Geometry of Interaction 1: Interpretation of System F. In Studies in Logic and the Foundations of Mathematics, R. Ferro, C. Bonotto, S. Valentini, and A. Zanardo (Eds.). Vol. 127. Elsevier, 221-260."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603124"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394774"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/10.3"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656"},{"key":"e_1_2_1_57_1","unstructured":"Jean-Louis Krivine. 1993. Lambda-calculus types and models. Masson."},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","unstructured":"Jean-Louis Krivine. 2007. A Call-by-name Lambda-calculus Machine. Higher Order Symbol. Comput. 20 3 ( 2007 ) 199-207. https:\/\/doi.org\/10.1007\/s10990-007-9018-9 10.1007\/s10990-007-9018-9","DOI":"10.1007\/s10990-007-9018-9"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_23"},{"key":"e_1_2_1_60_1","unstructured":"Jean-Jacques L\u00e9vy. 1978. R\u00e9ductions correctes et optimales dans le lambda-calcul. PhD Thesis. Universit\u00e9 Paris 7."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199483"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-55386-2_16"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158094"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47666-6_28"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","unstructured":"Robin Milner. 1977. Fully Abstract Models of Typed lambda-Calculi. Theor. Comput. Sci. 4 1 ( 1977 ) 1-22. https: \/\/doi.org\/10.1016\/ 0304-3975 ( 77 ) 90053-6 10.1016\/0304-3975(77)90053-6","DOI":"10.1016\/0304-3975(77)90053-6"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL"},{"key":"e_1_2_1_68_1","volume-title":"Ghica","author":"Muroya Koko","year":"2019","unstructured":"Koko Muroya and Dan R. Ghica. 2019. The Dynamic Geometry of Interaction Machine: A Token-Guided Graph Rewriter. Log. Methods Comput. Sci. 15, 4 ( 2019 ). https:\/\/lmcs.episciences. org\/5882"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/1016850.1016871"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/1243996.1243997"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_30"},{"key":"e_1_2_1_73_1","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"Pottinger Garrel","unstructured":"Garrel Pottinger. 1980. A Type Assignment for The Strongly Normalizable \u03bb-terms. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J.P. Seldin and J.R. Hindley (Eds.). Academic Press, 561-578."},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36377-7_4"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.45"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","unstructured":"Ulrich Sch\u00f6pp. 2014. On the Relation of Interaction Semantics to Continuations and Defunctionalization. Logical Methods in Computer Science 10 4 ( 2014 ). https:\/\/doi.org\/10.2168\/LMCS-10 ( 4 :10) 2014 10.2168\/LMCS-10(4:10)2014","DOI":"10.2168\/LMCS-10"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26529-2_14"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434332","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434332","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T07:26:54Z","timestamp":1781854014000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434332"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":78,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2021,1,4]]}},"alternative-id":["10.1145\/3434332"],"URL":"https:\/\/doi.org\/10.1145\/3434332","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,1,4]]},"assertion":[{"value":"2021-01-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}