{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:14:13Z","timestamp":1750220053070,"version":"3.41.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"ANR","award":["ANR-19-CE48-0010-01"],"award-info":[{"award-number":["ANR-19-CE48-0010-01"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,1,9]]},"abstract":"<jats:p>We introduce a multi-token machine for Idealized Parallel Algol (IPA), a higher-order concurrent programming language with shared state and semaphores. Our machine takes the shape of a compositional interpretation of terms as Petri structures, certain coloured Petri nets. For the purely functional fragment of IPA, our machine is conceptually close to Geometry of Interaction token machines, originating from Linear Logic and presenting higher-order computation as the low-level process of a token walking through a graph (a proof net) representing the term. We combine here these ideas with folklore ideas on the representation of first-order imperative concurrent programs as coloured Petri nets.<\/jats:p>\n          <jats:p>To prove our machine computationally adequate with respect to the reference operational semantics, we follow game semantics and represent types as certain games specifying dependencies and conflict between computational events. Petri strategies are those Petri structures obeying the rules of the game extracted from the type. We show how Petri strategies unfold to concurrent strategies in the sense of concurrent games on event structures. This link with concurrent strategies not only allows us to prove adequacy of our machine, but also lets us generate operationally a causal description of the behaviour of programs at higher-order types, which is shown to coincide with that given denotationally by the interpretation in concurrent games.<\/jats:p>","DOI":"10.1145\/3571217","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"689-717","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal Unfolding"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5886-5793","authenticated-orcid":false,"given":"Simon","family":"Castellan","sequence":"first","affiliation":[{"name":"University of Rennes, France \/ Inria, France \/ CNRS, France \/ IRISA, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3285-6028","authenticated-orcid":false,"given":"Pierre","family":"Clairambault","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Aix-Marseille, France \/ Universit\u00e9 de Toulon, France \/ CNRS, France \/ LIS, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"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.1017\/S0960129520000043"},{"key":"e_1_2_1_3_1","unstructured":"Patrick Baillot. 1999. Approches dynamiques en s\u00e9mantique de la logique lin\u00e9aire: jeux et g\u00e9om\u00e9trie de l\u2019interaction. Ph. D. Dissertation. Aix-Marseille 2. \t\t\t\t  Patrick Baillot. 1999. Approches dynamiques en s\u00e9mantique de la logique lin\u00e9aire: jeux et g\u00e9om\u00e9trie de l\u2019interaction. Ph. D. Dissertation. Aix-Marseille 2."},{"key":"e_1_2_1_4_1","unstructured":"Simon Castellan and Pierre Clairambault. 2020. Disentangling Parallelism and Interference in Game Semantics. arxiv:2103.15453 Submitted \t\t\t\t  Simon Castellan and Pierre Clairambault. 2020. Disentangling Parallelism and Interference in Game Semantics. arxiv:2103.15453 Submitted"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209187"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(3:35)2017"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2014.10.006"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13675-7_11"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371131"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603154"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.58"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017","author":"Lago Ugo Dal","year":"2017","unstructured":"Ugo Dal Lago , Claudia Faggian , Beno\u00eet Valiron , and Akira Yoshimizu . 2017 . The geometry of parallelism: classical, probabilistic, and quantum effects . In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017 , Paris, France , January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 833\u2013845. http:\/\/dl.acm.org\/citation.cfm?id=3009859 Ugo Dal Lago, Claudia Faggian, Beno\u00eet Valiron, and Akira Yoshimizu. 2017. The geometry of parallelism: classical, probabilistic, and quantum effects. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 833\u2013845. http:\/\/dl.acm.org\/citation.cfm?id=3009859"},{"volume-title":"The geometry of concurrent interaction: Handling multiple ports by way of multiple tokens","author":"Lago Ugo Dal","key":"e_1_2_1_13_1","unstructured":"Ugo Dal Lago , Ryo Tanaka , and Akira Yoshimizu . 2017. The geometry of concurrent interaction: Handling multiple ports by way of multiple tokens . In LICS. IEEE Computer Society , 1\u201312. Ugo Dal Lago, Ryo Tanaka, and Akira Yoshimizu. 2017. The geometry of concurrent interaction: Handling multiple ports by way of multiple tokens. In LICS. IEEE Computer Society, 1\u201312."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561456"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80402-5"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.11.027"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2007.10.005"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2012.08.013"},{"volume-title":"Studies in Logic and the Foundations of Mathematics. 127","author":"Girard Jean-Yves","key":"e_1_2_1_19_1","unstructured":"Jean-Yves Girard . 1989. Geometry of interaction 1: Interpretation of System F . In Studies in Logic and the Foundations of Mathematics. 127 , Elsevier , 221\u2013260. Jean-Yves Girard. 1989. Geometry of interaction 1: Interpretation of System F. In Studies in Logic and the Foundations of Mathematics. 127, Elsevier, 221\u2013260."},{"volume-title":"Geometry of interaction III: accommodating the additives","author":"Girard Jean-Yves","key":"e_1_2_1_20_1","unstructured":"Jean-Yves Girard . 1995. Geometry of interaction III: accommodating the additives . London Mathematical Society Lecture Note Series , 329\u2013389. Jean-Yves Girard. 1995. Geometry of interaction III: accommodating the additives. London Mathematical Society Lecture Note Series, 329\u2013389."},{"volume-title":"The Geometry of Optimal Lambda Reduction","author":"Gonthier Georges","key":"e_1_2_1_21_1","unstructured":"Georges Gonthier , Mart\u00edn Abadi , and Jean-Jacques L\u00e9vy . 1992. The Geometry of Optimal Lambda Reduction . In POPL. ACM Press , 15\u201326. Georges Gonthier, Mart\u00edn Abadi, and Jean-Jacques L\u00e9vy. 1992. The Geometry of Optimal Lambda Reduction. In POPL. ACM Press, 15\u201326."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2016.10.010"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2008.1755"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603124"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2917"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_17"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73420-8_58"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_23"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603150"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199483"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_6"},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Koko Muroya Naohiko Hoshino and Ichiro Hasuo. 2016. Memoryful geometry of interaction II: recursion and adequacy. In POPL. ACM 748\u2013760. \t\t\t\t  Koko Muroya Naohiko Hoshino and Ichiro Hasuo. 2016. Memoryful geometry of interaction II: recursion and adequacy. In POPL. ACM 748\u2013760.","DOI":"10.1145\/2914770.2837672"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90112-2"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48068-4_20"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676985"},{"key":"e_1_2_1_36_1","volume-title":"Advances in Petri Nets (Lecture Notes in Computer Science","volume":"392","author":"Winskel Glynn","year":"1986","unstructured":"Glynn Winskel . 1986 . Event Structures . In Advances in Petri Nets (Lecture Notes in Computer Science , Vol. 255). Springer, 325\u2013 392 . Glynn Winskel. 1986. Event Structures. In Advances in Petri Nets (Lecture Notes in Computer Science, Vol. 255). Springer, 325\u2013392."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571217","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571217","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:21Z","timestamp":1750183701000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571217"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":36,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571217"],"URL":"https:\/\/doi.org\/10.1145\/3571217","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}