{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,13]],"date-time":"2026-05-13T01:19:14Z","timestamp":1778635154865,"version":"3.51.4"},"reference-count":112,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101003349"],"award-info":[{"award-number":["101003349"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100008398","name":"Villum Fonden","doi-asserted-by":"publisher","award":["25804"],"award-info":[{"award-number":["25804"]}],"id":[{"id":"10.13039\/100008398","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":[[2024,1,2]]},"abstract":"<jats:p>\n            We introduce a linear concurrent separation logic, called\n            <jats:bold>LinearActris<\/jats:bold>\n            , designed to guarantee deadlock and leak freedom for message-passing concurrency. LinearActris combines the strengths of session types and concurrent separation logic, allowing for the verification of challenging higher-order programs with mutable state through dependent protocols. The key challenge is to prove the adequacy theorem of LinearActris, which says that the logic indeed gives deadlock and leak freedom \u201cfor free\u201d from linearity. We prove this theorem by defining a step-indexed model of separation logic, based on\n            <jats:italic toggle=\"yes\">connectivity graphs<\/jats:italic>\n            . To demonstrate the expressive power of LinearActris, we prove soundness of a higher-order (GV-style) session type system using the technique of logical relations. All our results and examples have been mechanized in Coq.\n          <\/jats:p>","DOI":"10.1145\/3632889","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"1385-1417","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1976-3182","authenticated-orcid":false,"given":"Jules","family":"Jacobs","sequence":"first","affiliation":[{"name":"Radboud University Nijmegen, Nijmegen, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6143-9031","authenticated-orcid":false,"given":"Jonas Kastberg","family":"Hinrichsen","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus N, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1185-5237","authenticated-orcid":false,"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Nijmegen, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/1037736"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","unstructured":"Amal Ahmed Andrew W. Appel Christopher D. Richards Kedar N. Swadi Gang Tan and Daniel C. Wang. 2010. Semantic foundations for typed assembly languages. TOPLAS (2010). https:\/\/doi.org\/10.1145\/1709093.1709094 10.1145\/1709093.1709094","DOI":"10.1145\/1709093.1709094"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","unstructured":"Pierre America and Jan J. M. M. Rutten. 1989. Solving Reflexive Domain Equations in a Category of Complete Metric Spaces. JCSS (1989). https:\/\/doi.org\/10.1016\/0022-0000(89)90027-5 10.1016\/0022-0000(89)90027-5","DOI":"10.1016\/0022-0000(89)90027-5"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","unstructured":"Andrew W. Appel. 2014. Program Logics for Certified Compilers. https:\/\/doi.org\/10.1017\/CBO9781107256552 10.1017\/CBO9781107256552","DOI":"10.1017\/CBO9781107256552"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","unstructured":"Andrew W. Appel and David McAllester. 2001. An Indexed Model of Recursive Types for Foundational Proof-Carrying Code. TOPLAS (2001). https:\/\/doi.org\/10.1145\/504709.504712 10.1145\/504709.504712","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","unstructured":"Andrew W. Appel Paul-Andr\u00e9 Melli\u00e8s Christopher D. Richards and J\u00e9r\u00f4me Vouillon. 2007. A very modal model of a modern major general type system. In POPL. https:\/\/doi.org\/10.1145\/1190216.1190235 10.1145\/1190216.1190235","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","unstructured":"Stephanie Balzer Frank Pfenning and Bernardo Toninho. 2018. A Universal Session Type for Untyped Asynchronous Communication. In CONCUR. https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2018.30 10.4230\/LIPIcs.CONCUR.2018.30","DOI":"10.4230\/LIPIcs.CONCUR.2018.30"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","unstructured":"Stephanie Balzer Bernardo Toninho and Frank Pfenning. 2019. Manifest Deadlock-Freedom for Shared Session Types. In ESOP. https:\/\/doi.org\/10.1007\/978-3-030-17184-1_22 10.1007\/978-3-030-17184-1_22","DOI":"10.1007\/978-3-030-17184-1_22"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","unstructured":"Nick Benton. 1994. A Mixed Linear and Non-Linear Logic: Proofs Terms and Models (Extended Abstract). In CSL. https:\/\/doi.org\/10.1007\/BFb0022251 10.1007\/BFb0022251","DOI":"10.1007\/BFb0022251"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","unstructured":"Lars Birkedal Bernhard Reus Jan Schwinghammer Kristian St\u00f8vring Jacob Thamsborg and Hongseok Yang. 2011. Step-indexed kripke models over recursive worlds. In POPL. https:\/\/doi.org\/10.1145\/1926385.1926401 10.1145\/1926385.1926401","DOI":"10.1145\/1926385.1926401"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","unstructured":"Lars Birkedal Kristian St\u00f8vring and Jacob Thamsborg. 2010. The category-theoretic solution of recursive metric-space equations. TCS (2010). https:\/\/doi.org\/10.1016\/j.tcs.2010.07.010 10.1016\/j.tcs.2010.07.010","DOI":"10.1016\/j.tcs.2010.07.010"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","unstructured":"Ales Bizjak Daniel Gratzer Robbert Krebbers and Lars Birkedal. 2019. Iron: Managing obligations in higher-order concurrent separation logic. POPL (2019). https:\/\/doi.org\/10.1145\/3290378 10.1145\/3290378","DOI":"10.1145\/3290378"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","unstructured":"Laura Bocchi Kohei Honda Emilio Tuosto and Nobuko Yoshida. 2010. A Theory of Design-by-Contract for Distributed Multiparty Interactions. In CONCUR. https:\/\/doi.org\/10.1007\/978-3-642-15375-4_12 10.1007\/978-3-642-15375-4_12","DOI":"10.1007\/978-3-642-15375-4_12"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","unstructured":"Stephen D. Brookes. 2004. A Semantics for Concurrent Separation Logic. In CONCUR. https:\/\/doi.org\/10.1007\/978-3-540-28644-8_2 10.1007\/978-3-540-28644-8_2","DOI":"10.1007\/978-3-540-28644-8_2"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","unstructured":"Lu\u00eds Caires Jorge A. P\u00e9rez Frank Pfenning and Bernardo Toninho. 2013. Behavioral Polymorphism and Parametricity in Session-Based Communication. In ESOP. https:\/\/doi.org\/10.1007\/978-3-642-37036-6_19 10.1007\/978-3-642-37036-6_19","DOI":"10.1007\/978-3-642-37036-6_19"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","unstructured":"Lu\u00eds Caires and Frank Pfenning. 2010. Session Types as Intuitionistic Linear Propositions. In CONCUR. https:\/\/doi.org\/10.1007\/978-3-642-15375-4_16 10.1007\/978-3-642-15375-4_16","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","unstructured":"Qinxiang Cao Lennart Beringer Samuel Gruetter Josiah Dodds and Andrew W. Appel. 2018. VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs. JAR (2018). https:\/\/doi.org\/10.1007\/s10817-018-9457-5 10.1007\/s10817-018-9457-5","DOI":"10.1007\/s10817-018-9457-5"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","unstructured":"Qinxiang Cao Santiago Cuellar and Andrew W. Appel. 2017. Bringing Order to the Separation Logic Jungle. In APLAS. https:\/\/doi.org\/10.1007\/978-3-319-71237-6_10 10.1007\/978-3-319-71237-6_10","DOI":"10.1007\/978-3-319-71237-6_10"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","unstructured":"Marco Carbone and S\u00f8ren Debois. 2010. A Graphical Approach to Progress for Structured Communication in Web Services. In ICE. https:\/\/doi.org\/10.4204\/EPTCS.38.4 10.4204\/EPTCS.38.4","DOI":"10.4204\/EPTCS.38.4"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","unstructured":"Marco Carbone Sam Lindley Fabrizio Montesi Carsten Sch\u00fcrmann and Philip Wadler. 2016. Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types. In CONCUR. https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2016.33 10.4230\/LIPIcs.CONCUR.2016.33","DOI":"10.4230\/LIPIcs.CONCUR.2016.33"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","unstructured":"Marco Carbone Fabrizio Montesi Carsten Sch\u00fcrmann and Nobuko Yoshida. 2015. Multiparty Session Types as Coherence Proofs. In CONCUR. https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2015.412 10.4230\/LIPIcs.CONCUR.2015.412","DOI":"10.4230\/LIPIcs.CONCUR.2015.412"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","unstructured":"Marco Carbone Fabrizio Montesi Carsten Sch\u00fcrmann and Nobuko Yoshida. 2017. Multiparty session types as coherence proofs. Acta Informatica (2017). https:\/\/doi.org\/10.1007\/s00236-016-0285-y 10.1007\/s00236-016-0285-y","DOI":"10.1007\/s00236-016-0285-y"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","unstructured":"David Castro-Perez Francisco Ferreira Lorenzo Gheri and Nobuko Yoshida. 2021. Zooid: A DSL for Certified Multiparty Computation: From Mechanised Metatheory to Certified Multiparty Processes. In PLDI. https:\/\/doi.org\/10.1145\/3453483.3454041 10.1145\/3453483.3454041","DOI":"10.1145\/3453483.3454041"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","unstructured":"David Castro-Perez Francisco Ferreira and Nobuko Yoshida. 2020. EMTST: Engineering the Meta-theory of Session Types. In TACAS. https:\/\/doi.org\/10.1007\/978-3-030-45237-7_17 10.1007\/978-3-030-45237-7_17","DOI":"10.1007\/978-3-030-45237-7_17"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","unstructured":"Arthur Chargu\u00e9raud. 2020. Separation logic for sequential programs (functional pearl). ICFP (2020). https:\/\/doi.org\/10.1145\/3408998 10.1145\/3408998","DOI":"10.1145\/3408998"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","unstructured":"Kaustuv Chaudhuri Leonardo Lima and Giselle Reis. 2019. Formalized Meta-Theory of Sequent Calculi for Linear Logics. TCS (2019). https:\/\/doi.org\/10.1016\/j.tcs.2019.02.023 10.1016\/j.tcs.2019.02.023","DOI":"10.1016\/j.tcs.2019.02.023"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","unstructured":"Adam Chlipala. 2013. The Bedrock structured programming system: combining generative metaprogramming and Hoare logic in an extensible program verifier. In ICFP. https:\/\/doi.org\/10.1145\/2500365.2500592 10.1145\/2500365.2500592","DOI":"10.1145\/2500365.2500592"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","unstructured":"Luca Ciccone and Luca Padovani. 2020. A Dependently Typed Linear \u03c0-Calculus in Agda. In PPDP. https:\/\/doi.org\/10.1145\/3414080.3414109 10.1145\/3414080.3414109","DOI":"10.1145\/3414080.3414109"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","unstructured":"Florin Craciun Tibor Kiss and Andreea Costea. 2015. Towards a Session Logic for Communication Protocols. In ICECCS. https:\/\/doi.org\/10.1109\/ICECCS.2015.33 10.1109\/ICECCS.2015.33","DOI":"10.1109\/ICECCS.2015.33"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","unstructured":"Lu\u00eds Cruz-Filipe Fabrizio Montesi and Marco Peressotti. 2021a. Certifying Choreography Compilation. In ICTAC. https:\/\/doi.org\/10.1007\/978-3-030-85315-0_8 10.1007\/978-3-030-85315-0_8","DOI":"10.1007\/978-3-030-85315-0_8"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","unstructured":"Lu\u00eds Cruz-Filipe Fabrizio Montesi and Marco Peressotti. 2021b. Formalising a Turing-Complete Choreographic Language in Coq. In ITP. https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2021.15 10.4230\/LIPIcs.ITP.2021.15","DOI":"10.4230\/LIPIcs.ITP.2021.15"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","unstructured":"Ornela Dardha and Simon J. Gay. 2018. A New Linear Logic for Deadlock-Free Session-Typed Processes. In FOSSACS. https:\/\/doi.org\/10.1007\/978-3-319-89366-2_5 10.1007\/978-3-319-89366-2_5","DOI":"10.1007\/978-3-319-89366-2_5"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","unstructured":"Ornela Dardha Elena Giachino and Davide Sangiorgi. 2012. Session types revisited. In PPDP. https:\/\/doi.org\/10.1145\/2370776.2370794 10.1145\/2370776.2370794","DOI":"10.1145\/2370776.2370794"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","unstructured":"Ankush Das Jan Hoffmann and Frank Pfenning. 2018. Work Analysis with Resource-Aware Session Types. In LICS. https:\/\/doi.org\/10.1145\/3209108.3209146 10.1145\/3209108.3209146","DOI":"10.1145\/3209108.3209146"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","unstructured":"Edsger W. Dijkstra. 1971. Hierarchical Ordering of Sequential Processes. Acta Informatica (1971). https:\/\/doi.org\/10.1007\/BF00289519 10.1007\/BF00289519","DOI":"10.1007\/BF00289519"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","unstructured":"Emanuele D\u2019Osualdo Julian Sutherland Azadeh Farzan and Philippa Gardner. 2021. TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs. TOPLAS (2021). https:\/\/doi.org\/10.1145\/3477082 10.1145\/3477082","DOI":"10.1145\/3477082"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","unstructured":"Derek Dreyer Amal Ahmed and Lars Birkedal. 2011. Logical step-indexed logical relations. LMCS (2011). https:\/\/doi.org\/10.2168\/LMCS-7(2:16)2011 10.2168\/LMCS-7(2:16)2011","DOI":"10.2168\/LMCS-7(2:16)2011"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","unstructured":"Simon Fowler Wen Kokke Ornela Dardha Sam Lindley and J. Garrett Morris. 2021. Separating Sessions Smoothly. In CONCUR. https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2021.36 10.4230\/LIPIcs.CONCUR.2021.36","DOI":"10.4230\/LIPIcs.CONCUR.2021.36"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","unstructured":"Simon Fowler Sam Lindley J. Garrett Morris and S\u00e1ra Decova. 2019. Exceptional Asynchronous Session Types: Session Types Without Tiers. POPL (2019). https:\/\/doi.org\/10.1145\/3290341 10.1145\/3290341","DOI":"10.1145\/3290341"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","unstructured":"Adrian Francalanza Julian Rathke and Vladimiro Sassone. 2011. Permission-Based Separation Logic for Message-Passing Concurrency. LMCS (2011). https:\/\/doi.org\/10.2168\/LMCS-7(3:7)2011 10.2168\/LMCS-7(3:7)2011","DOI":"10.2168\/LMCS-7(3:7)2011"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","unstructured":"Simon J. Gay and Vasco Thudichum Vasconcelos. 2010. Linear type theory for asynchronous session types. JFP (2010). https:\/\/doi.org\/10.1017\/S0956796809990268 10.1017\/S0956796809990268","DOI":"10.1017\/S0956796809990268"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","unstructured":"Leon Gondelman Jonas Kastberg Hinrichsen Mar\u00edo Pereira Amin Timany and Lars Birkedal. 2023. Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols. ICFP (2023). https:\/\/doi.org\/10.1145\/3607859 10.1145\/3607859","DOI":"10.1145\/3607859"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","unstructured":"Matthew A. Goto Radha Jagadeesan Alan Jeffrey Corin Pitcher and James Riely. 2016. An Extensible Approach to Session Polymorphism. MSCS (2016). https:\/\/doi.org\/10.1017\/S0960129514000231 10.1017\/S0960129514000231","DOI":"10.1017\/S0960129514000231"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","unstructured":"Jafar Hamin and Bart Jacobs. 2018. Deadlock-Free Monitors. In ESOP. https:\/\/doi.org\/10.1007\/978-3-319-89884-1_15 10.1007\/978-3-319-89884-1_15","DOI":"10.1007\/978-3-319-89884-1_15"},{"key":"e_1_3_1_46_1","doi-asserted-by":"crossref","unstructured":"Robert Harper. 2016. Practical Foundations for Programming Languages (2nd ed.).","DOI":"10.1017\/CBO9781316576892"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","unstructured":"Jonas Kastberg Hinrichsen Jesper Bengtson and Robbert Krebbers. 2020. Actris: Session-Type Based Reasoning in Separation Logic. POPL (2020). https:\/\/doi.org\/10.1145\/3371074 10.1145\/3371074","DOI":"10.1145\/3371074"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","unstructured":"Jonas Kastberg Hinrichsen Jesper Bengtson and Robbert Krebbers. 2022. Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic. LMCS (2022). https:\/\/doi.org\/10.46298\/lmcs-18(2:16)2022 10.46298\/lmcs-18(2:16)2022","DOI":"10.46298\/lmcs-18(2:16)2022"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","unstructured":"Jonas Kastberg Hinrichsen Dani\u00ebl Louwrink Robbert Krebbers and Jesper Bengtson. 2021. Machine-checked semantic session typing. In CPP. https:\/\/doi.org\/10.1145\/3437992.3439914 10.1145\/3437992.3439914","DOI":"10.1145\/3437992.3439914"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","unstructured":"Aquinas Hobor Andrew W. Appel and Francesco Zappa Nardelli. 2008. Oracle Semantics for Concurrent Separation Logic. In ESOP. https:\/\/doi.org\/10.1007\/978-3-540-78739-6_27 10.1007\/978-3-540-78739-6_27","DOI":"10.1007\/978-3-540-78739-6_27"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","unstructured":"Kohei Honda. 1993. Types for Dyadic Interaction. In CONCUR. https:\/\/doi.org\/10.1007\/3-540-57208-2_35 10.1007\/3-540-57208-2_35","DOI":"10.1007\/3-540-57208-2_35"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","unstructured":"Kohei Honda Vasco Thudichum Vasconcelos and Makoto Kubo. 1998. Language Primitives and Type Discipline for Structured Communication-Based Programming. In ESOP. https:\/\/doi.org\/10.1007\/BFb0053567 10.1007\/BFb0053567","DOI":"10.1007\/BFb0053567"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","unstructured":"Kohei Honda Nobuko Yoshida and Marco Carbone. 2008. Multiparty Asynchronous Session Types. In POPL. https:\/\/doi.org\/10.1145\/1328438.1328472 10.1145\/1328438.1328472","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","unstructured":"Kohei Honda Nobuko Yoshida and Marco Carbone. 2016. Multiparty Asynchronous Session Types. J. ACM (2016). https:\/\/doi.org\/10.1145\/2827695 10.1145\/2827695","DOI":"10.1145\/2827695"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","unstructured":"Atsushi Igarashi and Naoki Kobayashi. 1997. Type-Based Analysis of Communication for Concurrent Programming Languages. In SAS. https:\/\/doi.org\/10.1007\/BFb0032742 10.1007\/BFb0032742","DOI":"10.1007\/BFb0032742"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","unstructured":"Atsushi Igarashi and Naoki Kobayashi. 2001. A Generic Type System for the Pi-calculus. In POPL. https:\/\/doi.org\/10.1145\/360204.360215 10.1145\/360204.360215","DOI":"10.1145\/360204.360215"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","unstructured":"Atsushi Igarashi and Naoki Kobayashi. 2004. A Generic Type System for the Pi-calculus. TCS (2004). https:\/\/doi.org\/10.1016\/S0304-3975(03)00325-6 10.1016\/S0304-3975(03)00325-6","DOI":"10.1016\/S0304-3975(03)00325-6"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","unstructured":"Jules Jacobs. 2022. A Self-Dual Distillation of Session Types. In ECOOP. https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2022.23 10.4230\/LIPIcs.ECOOP.2022.23","DOI":"10.4230\/LIPIcs.ECOOP.2022.23"},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","unstructured":"Jules Jacobs and Stephanie Balzer. 2023. Higher-Order Leak and Deadlock Free Locks. POPL (2023). https:\/\/doi.org\/10.1145\/3571229 10.1145\/3571229","DOI":"10.1145\/3571229"},{"key":"e_1_3_1_60_1","doi-asserted-by":"publisher","unstructured":"Jules Jacobs Stephanie Balzer and Robbert Krebbers. 2022a. Connectivity graphs: a method for proving deadlock freedom based on separation logic. POPL (2022). https:\/\/doi.org\/10.1145\/3498662 10.1145\/3498662","DOI":"10.1145\/3498662"},{"key":"e_1_3_1_61_1","doi-asserted-by":"publisher","unstructured":"Jules Jacobs Stephanie Balzer and Robbert Krebbers. 2022b. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom. ICFP (2022). https:\/\/doi.org\/10.1145\/3547638 10.1145\/3547638","DOI":"10.1145\/3547638"},{"key":"e_1_3_1_62_1","doi-asserted-by":"publisher","unstructured":"Jules Jacobs Jonas Kastberg Hinrichsen and Robbert Krebbers. 2023a. Coq Mechanization of \u201cDeadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing\u201d. https:\/\/doi.org\/10.5281\/zenodo.8422755 10.5281\/zenodo.8422755","DOI":"10.5281\/zenodo.8422755"},{"key":"e_1_3_1_63_1","doi-asserted-by":"publisher","unstructured":"Jules Jacobs Jonas Kastberg Hinrichsen and Robbert Krebbers. 2023b. Dependent Session Protocols in Separation Logic from First Principles (Functional Pearl). ICFP (2023). https:\/\/doi.org\/10.1145\/3607856 10.1145\/3607856","DOI":"10.1145\/3607856"},{"key":"e_1_3_1_64_1","volume-title":"Understanding and Evolving the Rust Programming Language","author":"Jung Ralf","year":"2020","unstructured":"Ralf Jung. 2020. Understanding and Evolving the Rust Programming Language. Ph.D. Dissertation. Universit\u00e4t des Saarlandes."},{"key":"e_1_3_1_65_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung Jacques-Henri Jourdan Robbert Krebbers and Derek Dreyer. 2018a. RustBelt: Securing the Foundations of the Rust Programming Language. POPL (2018). https:\/\/doi.org\/10.1145\/3158154 10.1145\/3158154","DOI":"10.1145\/3158154"},{"key":"e_1_3_1_66_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Lars Birkedal and Derek Dreyer. 2016. Higher-order ghost state. In ICFP. https:\/\/doi.org\/10.1145\/2951913.2951943 10.1145\/2951913.2951943","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_3_1_67_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ales Bizjak Lars Birkedal and Derek Dreyer. 2018b. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. JFP (2018). https:\/\/doi.org\/10.1017\/S0956796818000151 10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_68_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung David Swasey Filip Sieczkowski Kasper Svendsen Aaron Turon Lars Birkedal and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In POPL. https:\/\/doi.org\/10.1145\/2676726.2676980 10.1145\/2676726.2676980","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_1_69_1","doi-asserted-by":"publisher","unstructured":"Naoki Kobayashi. 1997. A Partially Deadlock-Free Typed Process Calculus. In LICS. https:\/\/doi.org\/10.1109\/LICS.1997.614941 10.1109\/LICS.1997.614941","DOI":"10.1109\/LICS.1997.614941"},{"key":"e_1_3_1_70_1","doi-asserted-by":"publisher","unstructured":"Naoki Kobayashi. 2002. A Type System for Lock-Free Processes. I&C (2002). https:\/\/doi.org\/10.1006\/inco.2002.3171 10.1006\/inco.2002.3171","DOI":"10.1006\/inco.2002.3171"},{"key":"e_1_3_1_71_1","doi-asserted-by":"publisher","unstructured":"Naoki Kobayashi Benjamin C. Pierce and David N. Turner. 1999. Linearity and the pi-calculus. TOPLAS (1999). https:\/\/doi.org\/10.1145\/330249.330251 10.1145\/330249.330251","DOI":"10.1145\/330249.330251"},{"key":"e_1_3_1_72_1","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Jacques-Henri Jourdan Ralf Jung Joseph Tassarotti Jan-Oliver Kaiser Amin Timany Arthur Chargu\u00e9raud and Derek Dreyer. 2018. MoSeL: A General Extensible Modal Framework for Interactive Proofs in Separation Logic. ICFP (2018). https:\/\/doi.org\/10.1145\/3236772 10.1145\/3236772","DOI":"10.1145\/3236772"},{"key":"e_1_3_1_73_1","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Ralf Jung Ales Bizjak Jacques-Henri Jourdan Derek Dreyer and Lars Birkedal. 2017a. The Essence of Higher-Order Concurrent Separation Logic. In ESOP. https:\/\/doi.org\/10.1007\/978-3-662-54434-1_26 10.1007\/978-3-662-54434-1_26","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_3_1_74_1","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Amin Timany and Lars Birkedal. 2017b. Interactive Proofs in Higher-Order Concurrent Separation Logic. In POPL. https:\/\/doi.org\/10.1145\/3009837.3009855 10.1145\/3009837.3009855","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_3_1_75_1","doi-asserted-by":"publisher","unstructured":"Duy-Khanh Le Wei-Ngan Chin and Yong Meng Teo. 2013. An Expressive Framework for Verifying Deadlock Freedom. In ATVA. https:\/\/doi.org\/10.1007\/978-3-319-02444-8_21 10.1007\/978-3-319-02444-8_21","DOI":"10.1007\/978-3-319-02444-8_21"},{"key":"e_1_3_1_76_1","doi-asserted-by":"publisher","unstructured":"K. Rustan M. Leino Peter M\u00fcller and Jan Smans. 2010. Deadlock-Free Channels and Locks. In ESOP. https:\/\/doi.org\/10.1007\/978-3-642-11957-6_22 10.1007\/978-3-642-11957-6_22","DOI":"10.1007\/978-3-642-11957-6_22"},{"key":"e_1_3_1_77_1","doi-asserted-by":"publisher","unstructured":"Hongjin Liang and Xinyu Feng. 2016. A program logic for concurrent objects under fair scheduling. In POPL. https:\/\/doi.org\/10.1145\/2837614.2837635 10.1145\/2837614.2837635","DOI":"10.1145\/2837614.2837635"},{"key":"e_1_3_1_78_1","doi-asserted-by":"publisher","unstructured":"Hongjin Liang and Xinyu Feng. 2018. Progress of concurrent objects with partial methods. POPL (2018). https:\/\/doi.org\/10.1145\/3158108 10.1145\/3158108","DOI":"10.1145\/3158108"},{"key":"e_1_3_1_79_1","doi-asserted-by":"publisher","unstructured":"Sam Lindley and J. Garrett Morris. 2015. A Semantics for Propositions as Sessions. In ESOP. https:\/\/doi.org\/10.1007\/978-3-662-46669-8_23 10.1007\/978-3-662-46669-8_23","DOI":"10.1007\/978-3-662-46669-8_23"},{"key":"e_1_3_1_80_1","doi-asserted-by":"publisher","unstructured":"Sam Lindley and J. Garrett Morris. 2016. Talking Bananas: Structural Recursion For Session Types. In ICFP. https:\/\/doi.org\/10.1145\/2951913.2951921 10.1145\/2951913.2951921","DOI":"10.1145\/2951913.2951921"},{"key":"e_1_3_1_81_1","unstructured":"Sam Lindley and J. Garrett Morris. 2017. Lightweight Functional Session Types. In Behavioural Types: from Theory to Tools."},{"key":"e_1_3_1_82_1","doi-asserted-by":"publisher","unstructured":"\u00c9tienne Lozes and Jules Villard. 2011. Reliable Contracts for Unreliable Half-Duplex Communications. In Web Services and Formal Methods (WS-FM). https:\/\/doi.org\/10.1007\/978-3-642-29834-9_2 10.1007\/978-3-642-29834-9_2","DOI":"10.1007\/978-3-642-29834-9_2"},{"key":"e_1_3_1_83_1","doi-asserted-by":"publisher","unstructured":"\u00c9tienne Lozes and Jules Villard. 2012. Shared Contract-Obedient Endpoints. In ICE. https:\/\/doi.org\/10.4204\/EPTCS.104.3 10.4204\/EPTCS.104.3","DOI":"10.4204\/EPTCS.104.3"},{"key":"e_1_3_1_84_1","doi-asserted-by":"publisher","unstructured":"William Mansky. 2022. Bringing Iris into the Verified Software Toolchain. https:\/\/doi.org\/10.48550\/arXiv.2207.0657410.48550\/arXiv.2207.06574 10.48550\/arXiv.2207.0657410.48550\/arXiv.2207.06574","DOI":"10.48550\/arXiv.2207.0657410.48550\/arXiv.2207.06574"},{"key":"e_1_3_1_85_1","doi-asserted-by":"publisher","unstructured":"William Mansky Andrew W. Appel and Aleksey Nogin. 2017. A verified messaging system. OOPSLA (2017). https:\/\/doi.org\/10.1145\/3133911 10.1145\/3133911","DOI":"10.1145\/3133911"},{"key":"e_1_3_1_86_1","volume-title":"Introduction to Choreographies","author":"Montesi Fabrizio","year":"2021","unstructured":"Fabrizio Montesi. 2021. Introduction to Choreographies. (2021). Accepted for publication by Cambridge University Press."},{"key":"e_1_3_1_87_1","doi-asserted-by":"publisher","unstructured":"Hiroshi Nakano. 2000. A modality for recursion. In LICS. https:\/\/doi.org\/10.1109\/LICS.2000.855774 10.1109\/LICS.2000.855774","DOI":"10.1109\/LICS.2000.855774"},{"key":"e_1_3_1_88_1","doi-asserted-by":"publisher","unstructured":"Peter W. O\u2019Hearn. 2004. Resources Concurrency and Local Reasoning. In CONCUR. https:\/\/doi.org\/10.1007\/978-3-540-28644-8_4 10.1007\/978-3-540-28644-8_4","DOI":"10.1007\/978-3-540-28644-8_4"},{"key":"e_1_3_1_89_1","doi-asserted-by":"publisher","unstructured":"Peter W. O\u2019Hearn John C. Reynolds and Hongseok Yang. 2001. Local Reasoning about Programs that Alter Data Structures. In CSL. https:\/\/doi.org\/10.1007\/3-540-44802-0_1 10.1007\/3-540-44802-0_1","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_1_90_1","doi-asserted-by":"publisher","unstructured":"Wytse Oortwijn Stefan Blom and Marieke Huisman. 2016. Future-based Static Analysis of Message Passing Programs. In PLACES. https:\/\/doi.org\/10.4204\/EPTCS.211.7 10.4204\/EPTCS.211.7","DOI":"10.4204\/EPTCS.211.7"},{"key":"e_1_3_1_91_1","doi-asserted-by":"publisher","unstructured":"Luca Padovani. 2014. Deadlock and lock freedom in the linear \u03c0-calculus. In LICS. https:\/\/doi.org\/10.1145\/2603088.2603116 10.1145\/2603088.2603116","DOI":"10.1145\/2603088.2603116"},{"key":"e_1_3_1_92_1","doi-asserted-by":"publisher","unstructured":"Jorge A. P\u00e9rez Lu\u00eds Caires Frank Pfenning and Bernardo Toninho. 2014. Linear Logical Relations and Observational Equivalences for Session-Based Concurrency. I&C (2014). https:\/\/doi.org\/10.1016\/j.ic.2014.08.001 10.1016\/j.ic.2014.08.001","DOI":"10.1016\/j.ic.2014.08.001"},{"key":"e_1_3_1_93_1","doi-asserted-by":"publisher","unstructured":"Frank Pfenning and Dennis Griffith. 2015. Polarized Substructural Session Types. In FoSSaCS. https:\/\/doi.org\/10.1007\/978-3-662-46678-0_1 10.1007\/978-3-662-46678-0_1","DOI":"10.1007\/978-3-662-46678-0_1"},{"key":"e_1_3_1_94_1","unstructured":"Benjamin C. Pierce. 2002. Types and Programming Languages (1st ed.)."},{"key":"e_1_3_1_95_1","doi-asserted-by":"publisher","unstructured":"Zesen Qian G. A. Kavvos and Lars Birkedal. 2021. Client-Server Sessions in Linear Logic. ICFP (2021). https:\/\/doi.org\/10.1145\/3473567 10.1145\/3473567","DOI":"10.1145\/3473567"},{"key":"e_1_3_1_96_1","volume-title":"A Hybrid Logical Framework","author":"Reed Jason","year":"2009","unstructured":"Jason Reed. 2009a. A Hybrid Logical Framework. Ph. D. Dissertation. Carnegie Mellon University."},{"key":"e_1_3_1_97_1","unstructured":"Jason Reed. 2009b. A Judgmental Deconstruction of Modal Logic. (2009). http:\/\/www.cs.cmu.edu\/~jcreed\/papers\/jdml.pdf Unpublished manuscript."},{"key":"e_1_3_1_98_1","doi-asserted-by":"publisher","unstructured":"Pedro Rocha and Lu\u00eds Caires. 2021. Propositions-as-types and shared state. ICFP (2021). https:\/\/doi.org\/10.1145\/3473584 10.1145\/3473584","DOI":"10.1145\/3473584"},{"key":"e_1_3_1_99_1","doi-asserted-by":"publisher","unstructured":"Pedro Rocha and Lu\u00eds Caires. 2023. Safe Session-Based Concurrency with Shared Linear State. In ESOP. https:\/\/doi.org\/10.1007\/978-3-031-30044-8_16 10.1007\/978-3-031-30044-8_16","DOI":"10.1007\/978-3-031-30044-8_16"},{"key":"e_1_3_1_100_1","doi-asserted-by":"publisher","unstructured":"Arjen Rouvoet Casper Bach Poulsen Robbert Krebbers and Eelco Visser. 2020. Intrinsically-Typed Definitional Interpreters for Linear Session-Typed Languages. In CPP. https:\/\/doi.org\/10.1145\/3372885.3373818 10.1145\/3372885.3373818","DOI":"10.1145\/3372885.3373818"},{"key":"e_1_3_1_101_1","doi-asserted-by":"publisher","unstructured":"Alceste Scalas and Nobuko Yoshida. 2019. Less is more: multiparty session types revisited. POPL (2019). https:\/\/doi.org\/10.1145\/3290343 10.1145\/3290343","DOI":"10.1145\/3290343"},{"key":"e_1_3_1_102_1","doi-asserted-by":"publisher","unstructured":"Simon Spies Lennard G\u00e4her Daniel Gratzer Joseph Tassarotti Robbert Krebbers Derek Dreyer and Lars Birkedal. 2021. Transfinite Iris: resolving an existential dilemma of step-indexed separation logic. In PLDI. https:\/\/doi.org\/10.1145\/3453483.3454031 10.1145\/3453483.3454031","DOI":"10.1145\/3453483.3454031"},{"key":"e_1_3_1_103_1","doi-asserted-by":"publisher","unstructured":"Kasper Svendsen and Lars Birkedal. 2014. Impredicative concurrent abstract predicates. In ESOP. https:\/\/doi.org\/10.1007\/978-3-642-54833-8_9 10.1007\/978-3-642-54833-8_9","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_3_1_104_1","doi-asserted-by":"publisher","unstructured":"Joseph Tassarotti Ralf Jung and Robert Harper. 2017. A Higher-Order Logic for Concurrent Termination-Preserving Refinement. In ESOP. https:\/\/doi.org\/10.1007\/978-3-662-54434-1_34 10.1007\/978-3-662-54434-1_34","DOI":"10.1007\/978-3-662-54434-1_34"},{"key":"e_1_3_1_105_1","doi-asserted-by":"publisher","unstructured":"Peter Thiemann. 2019. Intrinsically-Typed Mechanized Semantics for Session Types. In PPDP. https:\/\/doi.org\/10.1145\/3354166.3354184 10.1145\/3354166.3354184","DOI":"10.1145\/3354166.3354184"},{"key":"e_1_3_1_106_1","unstructured":"Amin Timany Robbert Krebbers Derek Dreyer and Lars Birkedal. 2022. A Logical Approach to Type Soundness. Manuscript."},{"key":"e_1_3_1_107_1","volume-title":"A Logical Foundation for Session-Based Concurrent Computation","author":"Toninho Bernardo","year":"2015","unstructured":"Bernardo Toninho. 2015. A Logical Foundation for Session-Based Concurrent Computation. Ph.D. Dissertation. Carnegie Mellon University and New University of Lisbon."},{"key":"e_1_3_1_108_1","doi-asserted-by":"publisher","unstructured":"Bernardo Toninho Lu\u00eds Caires and Frank Pfenning. 2013. Higher-Order Processes Functions and Sessions: A Monadic Integration. In ESOP. https:\/\/doi.org\/10.1007\/978-3-642-37036-6_20 10.1007\/978-3-642-37036-6_20","DOI":"10.1007\/978-3-642-37036-6_20"},{"key":"e_1_3_1_109_1","doi-asserted-by":"publisher","unstructured":"Bernardo Toninho Lu\u00eds Caires and Frank Pfenning. 2014. Corecursion and Non-divergence in Session-Typed Processes. In Trustworthy Global Computing (LNCS Vol. 8902). 159\u2013175. https:\/\/doi.org\/10.1007\/978-3-662-45917-1_11 10.1007\/978-3-662-45917-1_11","DOI":"10.1007\/978-3-662-45917-1_11"},{"key":"e_1_3_1_110_1","doi-asserted-by":"publisher","unstructured":"Jules Villard \u00c9tienne Lozes and Cristiano Calcagno. 2009. Proving Copyless Message Passing. In APLAS. https:\/\/doi.org\/10.1007\/978-3-642-10672-9_15 10.1007\/978-3-642-10672-9_15","DOI":"10.1007\/978-3-642-10672-9_15"},{"key":"e_1_3_1_111_1","doi-asserted-by":"publisher","unstructured":"Philip Wadler. 2012. Propositions as sessions. In ICFP. https:\/\/doi.org\/10.1145\/2364527.2364568 10.1145\/2364527.2364568","DOI":"10.1145\/2364527.2364568"},{"key":"e_1_3_1_112_1","doi-asserted-by":"publisher","unstructured":"Andrew K. Wright and Matthias Felleisen. 1994. A Syntactic Approach to Type Soundness. I&C (1994). https:\/\/doi.org\/10.1006\/inco.1994.1093 10.1006\/inco.1994.1093","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_3_1_113_1","doi-asserted-by":"publisher","unstructured":"Dan Zhang Dragan Bosnacki Mark van den Brand Cornelis Huizing Bart Jacobs Ruurd Kuiper and Anton Wijs. 2016. Verifying Atomicity Preservation and Deadlock Freedom of a Generic Shared Variable Mechanism Used in Model-To-Code Transformations. In MODELSWARD. https:\/\/doi.org\/10.1007\/978-3-319-66302-9_13 10.1007\/978-3-319-66302-9_13","DOI":"10.1007\/978-3-319-66302-9_13"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632889","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632889","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:05:47Z","timestamp":1751659547000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632889"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":112,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632889"],"URL":"https:\/\/doi.org\/10.1145\/3632889","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}