{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:22:06Z","timestamp":1751660526282,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":52,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,9,8]],"date-time":"2020-09-08T00:00:00Z","timestamp":1599523200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100008952","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\/501100008952","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100011199","name":"European Research Council","doi-asserted-by":"publisher","award":["CoG 818616"],"award-info":[{"award-number":["CoG 818616"]}],"id":[{"id":"10.13039\/100011199","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,9,8]]},"DOI":"10.1145\/3414080.3414108","type":"proceedings-article","created":{"date-parts":[[2020,9,21]],"date-time":"2020-09-21T23:11:58Z","timestamp":1600729918000},"page":"1-15","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["The Machinery of Interaction"],"prefix":"10.1145","author":[{"given":"Beniamino","family":"Accattoli","sequence":"first","affiliation":[{"name":"INRIA &amp; \u00c9cole Polytechnique, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ugo","family":"Dal Lago","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Bologna &amp; INRIA, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gabriele","family":"Vanoni","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Bologna &amp; INRIA, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,9,21]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129502003730"},{"key":"e_1_3_2_1_2_1","volume-title":"Proceedings of RTA\u201912(LIPIcs), Vol.\u00a015","author":"Accattoli Beniamino","year":"2012","unstructured":"Beniamino Accattoli . 2012 . An Abstract Factorization Theorem for Explicit Substitutions . In Proceedings of RTA\u201912(LIPIcs), Vol.\u00a015 . 6\u201321. Beniamino Accattoli. 2012. An Abstract Factorization Theorem for Explicit Substitutions. In Proceedings of RTA\u201912(LIPIcs), Vol.\u00a015. 6\u201321."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2018.10.003"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02508-3_3"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628154"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3131851.3131855"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3354166.3354169"},{"key":"e_1_3_2_1_8_1","volume-title":"Logical Methods in Computer Science 12, 1","author":"Accattoli Beniamino","year":"2016","unstructured":"Beniamino Accattoli and Ugo Dal\u00a0Lago . 2016. (Leftmost-Outermost) Beta Reduction is Invariant , Indeed. Logical Methods in Computer Science 12, 1 ( 2016 ). Beniamino Accattoli and Ugo Dal\u00a0Lago. 2016. (Leftmost-Outermost) Beta Reduction is Invariant, Indeed. Logical Methods in Computer Science 12, 1 (2016)."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679682000012X"},{"key":"e_1_3_2_1_10_1","volume-title":"Implementing Open Call-by-Value. In FSEN","author":"Accattoli Beniamino","year":"2017","unstructured":"Beniamino Accattoli and Giulio Guerrieri . 2017 . Implementing Open Call-by-Value. In FSEN 2017, Revised Selected Papers. 1\u201319. Beniamino Accattoli and Giulio Guerrieri. 2017. Implementing Open Call-by-Value. In FSEN 2017, Revised Selected Papers. 1\u201319."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15205-4_30"},{"key":"e_1_3_2_1_12_1","volume-title":"Proceedings of the 23rd RTA. 22\u201337","author":"Accattoli Beniamino","year":"2012","unstructured":"Beniamino Accattoli and Ugo\u00a0Dal Lago . 2012 . On the Invariance of the Unitary Cost Model for Head Reduction . In Proceedings of the 23rd RTA. 22\u201337 . Beniamino Accattoli and Ugo\u00a0Dal Lago. 2012. On the Invariance of the Unitary Cost Model for Head Reduction. In Proceedings of the 23rd RTA. 22\u201337."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Beniamino Accattoli Ugo\u00a0Dal Lago and Gabriele Vanoni. 2020. The Machinery of Interaction (Long Version). https:\/\/arxiv.org\/abs\/2002.05649.  Beniamino Accattoli Ugo\u00a0Dal Lago and Gabriele Vanoni. 2020. The Machinery of Interaction (Long Version). https:\/\/arxiv.org\/abs\/2002.05649.","DOI":"10.1145\/3414080.3414108"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.23"},{"key":"e_1_3_2_1_15_1","volume-title":"Proceedings of LICS \u201994","author":"Asperti Andrea","year":"1994","unstructured":"Andrea Asperti , Vincent Danos , Cosimo Laneve , and Laurent Regnier . 1994 . Paths in the lambda-calculus . In Proceedings of LICS \u201994 . 426\u2013436. Andrea Asperti, Vincent Danos, Cosimo Laneve, and Laurent Regnier. 1994. Paths in the lambda-calculus. In Proceedings of LICS \u201994. 426\u2013436."},{"key":"e_1_3_2_1_16_1","volume-title":"Blelloch and John Greiner","author":"E.","year":"1995","unstructured":"Guy\u00a0 E. Blelloch and John Greiner . 1995 . Parallelism in Sequential Functional Languages. In FPCA. 226\u2013237. Guy\u00a0E. Blelloch and John Greiner. 1995. Parallelism in Sequential Functional Languages. In FPCA. 226\u2013237."},{"key":"e_1_3_2_1_17_1","volume-title":"Proceedings of the 3rd FLOPS.","author":"Curien Pierre-Louis","year":"1998","unstructured":"Pierre-Louis Curien and Hugo Herbelin . 1998 . Computing with Abstract B\u00f6hm Trees . In Proceedings of the 3rd FLOPS. Pierre-Louis Curien and Hugo Herbelin. 1998. Computing with Abstract B\u00f6hm Trees. In Proceedings of the 3rd FLOPS."},{"key":"e_1_3_2_1_18_1","unstructured":"Pierre-Louis Curien and Hugo Herbelin. 2007. Abstract machines for dialogue games. (2007). arxiv:0706.2544http:\/\/arxiv.org\/abs\/0706.2544  Pierre-Louis Curien and Hugo Herbelin. 2007. Abstract machines for dialogue games. (2007). arxiv:0706.2544http:\/\/arxiv.org\/abs\/0706.2544"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603154"},{"key":"e_1_3_2_1_20_1","volume-title":"Proceedings of the 30th LICS. 559\u2013572","author":"Dal\u00a0Lago Ugo","year":"2015","unstructured":"Ugo Dal\u00a0Lago , Claudia Faggian , Beno\u00eet Valiron , and Akira Yoshimizu . 2015 . Parallelism and Synchronization in an Infinitary Context . In Proceedings of the 30th LICS. 559\u2013572 . Ugo Dal\u00a0Lago, Claudia Faggian, Beno\u00eet Valiron, and Akira Yoshimizu. 2015. Parallelism and Synchronization in an Infinitary Context. In Proceedings of the 30th LICS. 559\u2013572."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009859"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.01.044"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2015.04.006"},{"key":"e_1_3_2_1_24_1","volume-title":"Proceedings of the 32nd LICS. 1\u201312","author":"Dal\u00a0Lago Ugo","year":"2017","unstructured":"Ugo Dal\u00a0Lago , Ryo Tanaka , and Akira Yoshimizu . 2017 . The geometry of concurrent interaction: Handling multiple ports by way of multiple tokens . In Proceedings of the 32nd LICS. 1\u201312 . Ugo Dal\u00a0Lago, Ryo Tanaka, and Akira Yoshimizu. 2017. The geometry of concurrent interaction: Handling multiple ports by way of multiple tokens. In Proceedings of the 32nd LICS. 1\u201312."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561456"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1993.287578"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00049-3"},{"key":"e_1_3_2_1_29_1","volume-title":"3rd Working Conference on the Formal Description of Programming Concepts.","author":"Felleisen Matthias","year":"1986","unstructured":"Matthias Felleisen and Daniel\u00a0 P. Friedman . 1986 . Control operators, the SECD-machine, and the lambda-calculus . In 3rd Working Conference on the Formal Description of Programming Concepts. Matthias Felleisen and Daniel\u00a0P. Friedman. 1986. Control operators, the SECD-machine, and the lambda-calculus. In 3rd Working Conference on the Formal Description of Programming Concepts."},{"key":"e_1_3_2_1_30_1","volume-title":"Proceedings of the 1st ICGT. 75\u201389","author":"Fern\u00e1ndez Maribel","year":"2002","unstructured":"Maribel Fern\u00e1ndez and Ian Mackie . 2002 . Call-by-Value lambda-Graph Rewriting Without Rewriting . In Proceedings of the 1st ICGT. 75\u201389 . Maribel Fern\u00e1ndez and Ian Mackie. 2002. Call-by-Value lambda-Graph Rewriting Without Rewriting. In Proceedings of the 1st ICGT. 75\u201389."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"crossref","unstructured":"Yannick Forster Fabian Kunze and Marc Roth. 2019. The Weak Call-by-Value \u03bb-Calculus is Reasonable for Both Time and Space. PACMPL 4 POPL Article 27(2019) 23\u00a0pages.  Yannick Forster Fabian Kunze and Marc Roth. 2019. The Weak Call-by-Value \u03bb-Calculus is Reasonable for Both Time and Space. PACMPL 4 POPL Article 27(2019) 23\u00a0pages.","DOI":"10.1145\/3371095"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190269"},{"volume-title":"Studies in Logic and the Foundations of Mathematics, R.\u00a0Ferro, C.\u00a0Bonotto, S.\u00a0Valentini, and A.\u00a0Zanardo (Eds.). Vol.\u00a0127","author":"Girard Jean-Yves","key":"e_1_3_2_1_33_1","unstructured":"Jean-Yves Girard . 1989. Geometry of Interaction 1: Interpretation of System F . In Studies in Logic and the Foundations of Mathematics, R.\u00a0Ferro, C.\u00a0Bonotto, S.\u00a0Valentini, and A.\u00a0Zanardo (Eds.). Vol.\u00a0127 . Elsevier , 221\u2013260. Jean-Yves Girard. 1989. Geometry of Interaction 1: Interpretation of System F. In Studies in Logic and the Foundations of Mathematics, R.\u00a0Ferro, C.\u00a0Bonotto, S.\u00a0Valentini, and A.\u00a0Zanardo (Eds.). Vol.\u00a0127. Elsevier, 221\u2013260."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143172"},{"key":"e_1_3_2_1_35_1","first-page":"1","article-title":"Memoryful Geometry of Interaction: From Coalgebraic Components to Algebraic Effects(Proceedings of CSL-LICS \u201914)","volume":"52","author":"Hoshino Naohiko","year":"2014","unstructured":"Naohiko Hoshino , Koko Muroya , and Ichiro Hasuo . 2014 . Memoryful Geometry of Interaction: From Coalgebraic Components to Algebraic Effects(Proceedings of CSL-LICS \u201914) . ACM , 52 : 1 \u2013 52 :10. Naohiko Hoshino, Koko Muroya, and Ichiro Hasuo. 2014. Memoryful Geometry of Interaction: From Coalgebraic Components to Algebraic Effects(Proceedings of CSL-LICS \u201914). ACM, 52:1\u201352:10.","journal-title":"ACM"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100074338"},{"volume-title":"Milner\u2019s Lambda Calculus with Partial Substitutions","author":"Kesner Delia","key":"e_1_3_2_1_37_1","unstructured":"Delia Kesner and Shane\u00a0\u00d3 Conch\u00fair . 2008. Milner\u2019s Lambda Calculus with Partial Substitutions . Technical Report. Paris 7 University . http:\/\/www.pps.univ-paris-diderot.fr\/~kesner\/papers\/shortpartial.pdf. Delia Kesner and Shane\u00a0\u00d3 Conch\u00fair. 2008. Milner\u2019s Lambda Calculus with Partial Substitutions. Technical Report. Paris 7 University. http:\/\/www.pps.univ-paris-diderot.fr\/~kesner\/papers\/shortpartial.pdf."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9018-9"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/363744.363749"},{"key":"e_1_3_2_1_40_1","volume-title":"Proceedings of the 5th TLCA. 283\u2013297","author":"Laurent Olivier","year":"2001","unstructured":"Olivier Laurent . 2001 . A Token Machine for Full Geometry of Interaction . In Proceedings of the 5th TLCA. 283\u2013297 . Olivier Laurent. 2001. A Token Machine for Full Geometry of Interaction. In Proceedings of the 5th TLCA. 283\u2013297."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199483"},{"key":"e_1_3_2_1_42_1","volume-title":"System T. In Proceedings of the 24th WoLLIC. 229\u2013241","author":"Mackie Ian","year":"2017","unstructured":"Ian Mackie . 2017 . A Geometry of Interaction Machine for G\u00f6del\u2019s System T. In Proceedings of the 24th WoLLIC. 229\u2013241 . Ian Mackie. 2017. A Geometry of Interaction Machine for G\u00f6del\u2019s System T. In Proceedings of the 24th WoLLIC. 229\u2013241."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90263-1"},{"key":"e_1_3_2_1_44_1","volume-title":"Proceedings of the 24th CSL. 24\u201340","author":"Mazza Damiano","year":"2015","unstructured":"Damiano Mazza . 2015 . Simple Parsimonious Types and Logarithmic Space . In Proceedings of the 24th CSL. 24\u201340 . Damiano Mazza. 2015. Simple Parsimonious Types and Logarithmic Space. In Proceedings of the 24th CSL. 24\u201340."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-47666-6_28"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.07.035"},{"key":"e_1_3_2_1_47_1","volume-title":"Proceedings of the 26th CSL. 32:1\u201332:15","author":"Muroya Koko","year":"2017","unstructured":"Koko Muroya and Dan\u00a0 R. Ghica . 2017 . The Dynamic Geometry of Interaction Machine: A Call-by-Need Graph Rewriter . In Proceedings of the 26th CSL. 32:1\u201332:15 . Koko Muroya and Dan\u00a0R. Ghica. 2017. The Dynamic Geometry of Interaction Machine: A Call-by-Need Graph Rewriter. In Proceedings of the 26th CSL. 32:1\u201332:15."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90012-4"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/227699.227716"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"crossref","unstructured":"David Sands J\u00f6rgen Gustavsson and Andrew Moran. 2002. Lambda Calculi and Linear Speedups. In The Essence of Computation. 60\u201384.  David Sands J\u00f6rgen Gustavsson and Andrew Moran. 2002. Lambda Calculi and Linear Speedups. In The Essence of Computation. 60\u201384.","DOI":"10.1007\/3-540-36377-7_4"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.45"},{"key":"e_1_3_2_1_52_1","volume-title":"On the Relation of Interaction Semantics to Continuations and Defunctionalization. Logical Methods in Computer Science 10, 4","author":"Sch\u00f6pp Ulrich","year":"2014","unstructured":"Ulrich Sch\u00f6pp . 2014. On the Relation of Interaction Semantics to Continuations and Defunctionalization. Logical Methods in Computer Science 10, 4 ( 2014 ). Ulrich Sch\u00f6pp. 2014. On the Relation of Interaction Semantics to Continuations and Defunctionalization. Logical Methods in Computer Science 10, 4 (2014)."},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-26529-2_14"}],"event":{"name":"PPDP '20: 22nd International Symposium on Principles and Practice of Declarative Programming","acronym":"PPDP '20","location":"Bologna Italy"},"container-title":["Proceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3414080.3414108","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3414080.3414108","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:38:38Z","timestamp":1750199918000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3414080.3414108"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9,8]]},"references-count":52,"alternative-id":["10.1145\/3414080.3414108","10.1145\/3414080"],"URL":"https:\/\/doi.org\/10.1145\/3414080.3414108","relation":{},"subject":[],"published":{"date-parts":[[2020,9,8]]},"assertion":[{"value":"2020-09-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}