{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,1,29]],"date-time":"2024-01-29T16:05:12Z","timestamp":1706544312030},"reference-count":74,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-16-CE40-004-01"],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["GA 818616"],"id":[{"id":"10.13039\/501100000781","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":"\n Evaluating higher-order functional programs through abstract machines inspired by the geometry of the interaction is known to induce\n space<\/jats:italic>\n efficiencies, the price being\n 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 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-04T17:34:24Z","timestamp":1609781664000},"page":"1-33","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"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"}]},{"ORCID":"http:\/\/orcid.org\/0000-0001-9200-070X","authenticated-orcid":false,"given":"Ugo","family":"Dal Lago","sequence":"additional","affiliation":[{"name":"University of Bologna, Italy \/ Inria, France"}]},{"given":"Gabriele","family":"Vanoni","sequence":"additional","affiliation":[{"name":"University of Bologna, Italy \/ Inria, France"}]}],"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.2000.2930"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2018.10.003"},{"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.2012.22"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-12(1:4)2016"},{"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","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.2019.03.002"},{"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.2016.48"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1994.316048"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.10.002"},{"key":"e_1_2_1_18_1","unstructured":"Hendrik Pieter Barendregt. 1984. The lambda calculus: its syntax and semantics. North-Holland. 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","DOI":"10.2168\/LMCS-9(4:3)2013"},{"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","DOI":"10.2168\/LMCS-11(2:6)2015"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","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 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. 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 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.2015.58"},{"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.2015.04.006"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005112"},{"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.1996.561456"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1993.287578"},{"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","DOI":"10.1016\/S0304-3975(99)00049-3"},{"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. 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","DOI":"10.1017\/S0960129516000396"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.12.017"},{"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.2010.08.018"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","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. 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.2000.2917"},{"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.411"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103665"},{"key":"e_1_2_1_57_1","unstructured":"Jean-Louis Krivine. 1993. Lambda-calculus types and models. Masson. Jean-Louis Krivine. 1993. Lambda-calculus types and models. Masson."},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","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_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.2015.24"},{"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","DOI":"10.1016\/0304-3975(77)90053-6"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2017.32"},{"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 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.2006.38"},{"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. 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","DOI":"10.2168\/LMCS-10(4:10)2014"},{"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.2017.8005093"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3434332","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,2]],"date-time":"2023-01-02T00:51:13Z","timestamp":1672620673000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3434332"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,4]]},"references-count":74,"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":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}
