{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:08:29Z","timestamp":1750219709449,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":19,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,10,22]],"date-time":"2023-10-22T00:00:00Z","timestamp":1697932800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/R034567\/1"],"award-info":[{"award-number":["EP\/R034567\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003246","name":"Nederlandse Organisatie voor Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","award":["016.Vidi.189.046"],"award-info":[{"award-number":["016.Vidi.189.046"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,10,22]]},"DOI":"10.1145\/3610612.3610615","type":"proceedings-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T23:13:48Z","timestamp":1697498028000},"page":"1-14","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Termination in Concurrency, Revisited"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1711-9361","authenticated-orcid":false,"given":"Joseph W. N.","family":"Paulus","sequence":"first","affiliation":[{"name":"University of Groningen, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1452-6180","authenticated-orcid":false,"given":"Jorge A.","family":"P\u00e9rez","sequence":"additional","affiliation":[{"name":"University of Groningen, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1959-8730","authenticated-orcid":false,"given":"Daniele","family":"Nantes-Sobrinho","sequence":"additional","affiliation":[{"name":"Imperial College London, United Kingdom and University of Brasilia, Brazil"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,10,22]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"CONCUR 2010(LNCS, Vol.\u00a06269)","author":"Caires Lu\u00eds","year":"2010","unstructured":"Lu\u00eds Caires and Frank Pfenning . 2010 . Session Types as Intuitionistic Linear Propositions . In CONCUR 2010(LNCS, Vol.\u00a06269) . Springer, 222\u2013236. https:\/\/doi.org\/10.1007\/978-3-642-15375-4_16 10.1007\/978-3-642-15375-4_16 Lu\u00eds Caires and Frank Pfenning. 2010. Session Types as Intuitionistic Linear Propositions. In CONCUR 2010(LNCS, Vol.\u00a06269). Springer, 222\u2013236. https:\/\/doi.org\/10.1007\/978-3-642-15375-4_16"},{"key":"#cr-split#-e_1_3_2_1_2_1.1","doi-asserted-by":"crossref","unstructured":"Ornela Dardha Elena Giachino and Davide Sangiorgi. 2012. Session types revisited. In PPDP'12. ACM 139-150. https:\/\/doi.org\/10.1145\/2370776.2370794 10.1145\/2370776.2370794","DOI":"10.1145\/2370776.2370794"},{"key":"#cr-split#-e_1_3_2_1_2_1.2","doi-asserted-by":"crossref","unstructured":"Ornela Dardha Elena Giachino and Davide Sangiorgi. 2012. Session types revisited. In PPDP'12. ACM 139-150. https:\/\/doi.org\/10.1145\/2370776.2370794","DOI":"10.1145\/2370776.2370794"},{"key":"#cr-split#-e_1_3_2_1_3_1.1","doi-asserted-by":"crossref","unstructured":"Ornela Dardha and Jorge\u00a0A. P\u00e9rez. 2015. Comparing Deadlock-Free Session Typed Processes. In Combined 22th International Workshop on Expressiveness in Concurrency and 12th Workshop on Structural Operational Semantics and 12th Workshop on Structural Operational Semantics EXPRESS\/SOS(EPTCS Vol.\u00a0190). 1-15. https:\/\/doi.org\/10.4204\/EPTCS.190.1 10.4204\/EPTCS.190.1","DOI":"10.4204\/EPTCS.190.0"},{"key":"#cr-split#-e_1_3_2_1_3_1.2","doi-asserted-by":"crossref","unstructured":"Ornela Dardha and Jorge\u00a0A. P\u00e9rez. 2015. Comparing Deadlock-Free Session Typed Processes. In Combined 22th International Workshop on Expressiveness in Concurrency and 12th Workshop on Structural Operational Semantics and 12th Workshop on Structural Operational Semantics EXPRESS\/SOS(EPTCS Vol.\u00a0190). 1-15. https:\/\/doi.org\/10.4204\/EPTCS.190.1","DOI":"10.4204\/EPTCS.190.0"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","first-page":"100717","DOI":"10.1016\/j.jlamp.2021.100717","article-title":"Comparing type systems for deadlock freedom","volume":"124","author":"Dardha Ornela","year":"2022","unstructured":"Ornela Dardha and Jorge\u00a0 A. P\u00e9rez . 2022 . Comparing type systems for deadlock freedom . J. Log. Algebraic Methods Program. 124 (2022), 100717 . https:\/\/doi.org\/10.1016\/j.jlamp.2021.100717 10.1016\/j.jlamp.2021.100717 Ornela Dardha and Jorge\u00a0A. P\u00e9rez. 2022. Comparing type systems for deadlock freedom. J. Log. Algebraic Methods Program. 124 (2022), 100717. https:\/\/doi.org\/10.1016\/j.jlamp.2021.100717","journal-title":"J. Log. Algebraic Methods Program."},{"key":"e_1_3_2_1_5_1","volume-title":"CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR","author":"Demangeon Romain","year":"2010","unstructured":"Romain Demangeon , Daniel Hirschkoff , and Davide Sangiorgi . 2010. Termination in Impure Concurrent Languages . In CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010 , Paris, France, August 31-September 3, 2010. Proceedings(Lecture Notes in Computer Science, Vol.\u00a06269), Paul Gastin and Fran\u00e7ois Laroussinie (Eds.). Springer , 328\u2013342. https:\/\/doi.org\/10.1007\/978-3-642-15375-4_23 10.1007\/978-3-642-15375-4_23 Romain Demangeon, Daniel Hirschkoff, and Davide Sangiorgi. 2010. Termination in Impure Concurrent Languages. In CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings(Lecture Notes in Computer Science, Vol.\u00a06269), Paul Gastin and Fran\u00e7ois Laroussinie (Eds.). Springer, 328\u2013342. https:\/\/doi.org\/10.1007\/978-3-642-15375-4_23"},{"key":"e_1_3_2_1_6_1","volume-title":"Exploring New Frontiers of Theoretical Informatics, IFIP 18th World Computer Congress, TC1 3rd International Conference on Theoretical Computer Science (TCS2004)","author":"Deng Yuxin","year":"2004","unstructured":"Yuxin Deng and Davide Sangiorgi . 2004. Ensuring Termination by Typability . In Exploring New Frontiers of Theoretical Informatics, IFIP 18th World Computer Congress, TC1 3rd International Conference on Theoretical Computer Science (TCS2004) , 22-27 August 2004 , Toulouse, France( IFIP , Vol.\u00a0155), Jean-Jacques L\u00e9vy, Ernst\u00a0W. Mayr, and John\u00a0C. Mitchell (Eds.). Kluwer\/Springer , 619\u2013632. https:\/\/doi.org\/10.1007\/1-4020-8141-3_47 10.1007\/1-4020-8141-3_47 Yuxin Deng and Davide Sangiorgi. 2004. Ensuring Termination by Typability. In Exploring New Frontiers of Theoretical Informatics, IFIP 18th World Computer Congress, TC1 3rd International Conference on Theoretical Computer Science (TCS2004), 22-27 August 2004, Toulouse, France(IFIP, Vol.\u00a0155), Jean-Jacques L\u00e9vy, Ernst\u00a0W. Mayr, and John\u00a0C. Mitchell (Eds.). Kluwer\/Springer, 619\u2013632. https:\/\/doi.org\/10.1007\/1-4020-8141-3_47"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","first-page":"1045","DOI":"10.1016\/j.ic.2006.03.002","article-title":"Ensuring termination by typability","volume":"204","author":"Deng Yuxin","year":"2006","unstructured":"Yuxin Deng and Davide Sangiorgi . 2006 . Ensuring termination by typability . Information and Computation 204 , 7 (2006), 1045 \u2013 1082 . Yuxin Deng and Davide Sangiorgi. 2006. Ensuring termination by typability. Information and Computation 204, 7 (2006), 1045\u20131082.","journal-title":"Information and Computation"},{"volume-title":"ESOP\u201998(LNCS, Vol.\u00a01381)","author":"Honda Kohei","key":"e_1_3_2_1_8_1","unstructured":"Kohei Honda , Vasco\u00a0Thudichum Vasconcelos , and Makoto Kubo . 1998. Language Primitives and Type Discipline for Structured Communication-Based Programming . In ESOP\u201998(LNCS, Vol.\u00a01381) . Springer , 122\u2013138. https:\/\/doi.org\/10.1007\/BFb0053567 10.1007\/BFb0053567 Kohei Honda, Vasco\u00a0Thudichum Vasconcelos, and Makoto Kubo. 1998. Language Primitives and Type Discipline for Structured Communication-Based Programming. In ESOP\u201998(LNCS, Vol.\u00a01381). Springer, 122\u2013138. https:\/\/doi.org\/10.1007\/BFb0053567"},{"key":"e_1_3_2_1_9_1","article-title":"A hybrid type system for lock-freedom of mobile processes","volume":"32","author":"Kobayashi Naoki","year":"2010","unstructured":"Naoki Kobayashi and Davide Sangiorgi . 2010 . A hybrid type system for lock-freedom of mobile processes . ACM Trans. Program. Lang. Syst. 32 , 5 (2010), 16:1\u201316:49. https:\/\/doi.org\/10.1145\/1745312.1745313 10.1145\/1745312.1745313 Naoki Kobayashi and Davide Sangiorgi. 2010. A hybrid type system for lock-freedom of mobile processes. ACM Trans. Program. Lang. Syst. 32, 5 (2010), 16:1\u201316:49. https:\/\/doi.org\/10.1145\/1745312.1745313","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"e_1_3_2_1_10_1","volume-title":"Proc. ACM Program. Lang. 3, POPL","author":"Lago Ugo\u00a0Dal","year":"2019","unstructured":"Ugo\u00a0Dal Lago , Marc de Visme , Damiano Mazza , and Akira Yoshimizu . 2019 . Intersection types and runtime errors in the pi-calculus . Proc. ACM Program. Lang. 3, POPL (2019), 7:1\u20137:29. https:\/\/doi.org\/10.1145\/3290320 10.1145\/3290320 Ugo\u00a0Dal Lago, Marc de Visme, Damiano Mazza, and Akira Yoshimizu. 2019. Intersection types and runtime errors in the pi-calculus. Proc. ACM Program. Lang. 3, POPL (2019), 7:1\u20137:29. https:\/\/doi.org\/10.1145\/3290320"},{"key":"e_1_3_2_1_11_1","volume-title":"Revisited.","author":"Paulus Joseph","year":"2023","unstructured":"Joseph W.\u00a0N. Paulus , Jorge\u00a0 A. P\u00e9rez , and Daniele Nantes-Sobrinho . 2023. Termination in Concurrency , Revisited. ( 2023 ). arxiv:2308.01165https:\/\/doi.org\/10.48550\/arXiv.2308.01165 10.48550\/arXiv.2308.01165 Joseph W.\u00a0N. Paulus, Jorge\u00a0A. P\u00e9rez, and Daniele Nantes-Sobrinho. 2023. Termination in Concurrency, Revisited. (2023). arxiv:2308.01165https:\/\/doi.org\/10.48550\/arXiv.2308.01165"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","first-page":"254","DOI":"10.1016\/j.ic.2014.08.001","article-title":"Linear logical relations and observational equivalences for session-based concurrency","volume":"239","author":"P\u00e9rez A.","year":"2014","unstructured":"Jorge\u00a0 A. P\u00e9rez , Lu\u00eds Caires , Frank Pfenning , and Bernardo Toninho . 2014 . Linear logical relations and observational equivalences for session-based concurrency . Inf. Comput. 239 (2014), 254 \u2013 302 . https:\/\/doi.org\/10.1016\/j.ic.2014.08.001 10.1016\/j.ic.2014.08.001 Jorge\u00a0A. P\u00e9rez, Lu\u00eds Caires, Frank Pfenning, and Bernardo Toninho. 2014. Linear logical relations and observational equivalences for session-based concurrency. Inf. Comput. 239 (2014), 254\u2013302. https:\/\/doi.org\/10.1016\/j.ic.2014.08.001","journal-title":"Inf. Comput."},{"key":"e_1_3_2_1_13_1","first-page":"1","article-title":"Strong Normalization in the \u03c0 -calculus with Intersection and Union Types","volume":"121","author":"Piccolo Mauro","year":"2012","unstructured":"Mauro Piccolo . 2012 . Strong Normalization in the \u03c0 -calculus with Intersection and Union Types . Fundam. Informaticae 121 , 1 - 4 (2012), 227\u2013252. https:\/\/doi.org\/10.3233\/FI-2012-777 10.3233\/FI-2012-777 Mauro Piccolo. 2012. Strong Normalization in the \u03c0 -calculus with Intersection and Union Types. Fundam. Informaticae 121, 1-4 (2012), 227\u2013252. https:\/\/doi.org\/10.3233\/FI-2012-777","journal-title":"Fundam. Informaticae"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/S0960129505004810","article-title":"Termination of processes","volume":"16","author":"Sangiorgi Davide","year":"2006","unstructured":"Davide Sangiorgi . 2006 . Termination of processes . Math. Struct. Comput. Sci. 16 , 1 (2006), 1 \u2013 39 . https:\/\/doi.org\/10.1017\/S0960129505004810 10.1017\/S0960129505004810 Davide Sangiorgi. 2006. Termination of processes. Math. Struct. Comput. Sci. 16, 1 (2006), 1\u201339. https:\/\/doi.org\/10.1017\/S0960129505004810","journal-title":"Math. Struct. Comput. Sci."},{"key":"e_1_3_2_1_15_1","volume-title":"TGC 2014","author":"Toninho Bernardo","year":"2014","unstructured":"Bernardo Toninho , Lu\u00eds Caires , and Frank Pfenning . 2014 . Corecursion and Non-divergence in Session-Typed Processes. In Trustworthy Global Computing - 9th International Symposium , TGC 2014 , Rome, Italy , September 5-6, 2014. Revised Selected Papers(Lecture Notes in Computer Science, Vol.\u00a08902), Matteo Maffei and Emilio Tuosto (Eds.). Springer, 159\u2013175. https:\/\/doi.org\/10.1007\/978-3-662-45917-1_11 10.1007\/978-3-662-45917-1_11 Bernardo Toninho, Lu\u00eds Caires, and Frank Pfenning. 2014. Corecursion and Non-divergence in Session-Typed Processes. In Trustworthy Global Computing - 9th International Symposium, TGC 2014, Rome, Italy, September 5-6, 2014. Revised Selected Papers(Lecture Notes in Computer Science, Vol.\u00a08902), Matteo Maffei and Emilio Tuosto (Eds.). Springer, 159\u2013175. https:\/\/doi.org\/10.1007\/978-3-662-45917-1_11"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1016\/j.ic.2012.05.002","article-title":"Fundamentals of session types","volume":"217","author":"Vasconcelos T.","year":"2012","unstructured":"Vasco\u00a0 T. Vasconcelos . 2012 . Fundamentals of session types . Inf. Comput. 217 (2012), 52 \u2013 70 . https:\/\/doi.org\/10.1016\/j.ic.2012.05.002 10.1016\/j.ic.2012.05.002 Vasco\u00a0T. Vasconcelos. 2012. Fundamentals of session types. Inf. Comput. 217 (2012), 52\u201370. https:\/\/doi.org\/10.1016\/j.ic.2012.05.002","journal-title":"Inf. Comput."},{"key":"e_1_3_2_1_17_1","volume-title":"16th Annual IEEE Symposium on Logic in Computer Science","author":"Yoshida Nobuko","year":"2001","unstructured":"Nobuko Yoshida , Martin Berger , and Kohei Honda . 2001 . Strong Normalisation in the pi-Calculus . In 16th Annual IEEE Symposium on Logic in Computer Science , Boston, Massachusetts, USA , June 16-19, 2001, Proceedings. IEEE Computer Society, 311\u2013322. https:\/\/doi.org\/10.1109\/LICS.2001.932507 10.1109\/LICS.2001.932507 Nobuko Yoshida, Martin Berger, and Kohei Honda. 2001. Strong Normalisation in the pi-Calculus. In 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings. IEEE Computer Society, 311\u2013322. https:\/\/doi.org\/10.1109\/LICS.2001.932507"}],"event":{"name":"PPDP 2023: International Symposium on Principles and Practice of Declarative Programming","acronym":"PPDP 2023","location":"Lisboa Portugal"},"container-title":["International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3610612.3610615","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:36:00Z","timestamp":1750178160000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3610612.3610615"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,22]]},"references-count":19,"alternative-id":["10.1145\/3610612.3610615","10.1145\/3610612"],"URL":"https:\/\/doi.org\/10.1145\/3610612.3610615","relation":{},"subject":[],"published":{"date-parts":[[2023,10,22]]},"assertion":[{"value":"2023-10-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}