{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:13:03Z","timestamp":1760044383196,"version":"3.41.0"},"reference-count":90,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NSF","award":["CCF-1718267"],"award-info":[{"award-number":["CCF-1718267"]}]},{"name":"NWO","award":["016.Veni.192.259"],"award-info":[{"award-number":["016.Veni.192.259"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,1,16]]},"abstract":"<jats:p>\n            We introduce the notion of a\n            <jats:italic>connectivity graph<\/jats:italic>\n            \u2014an abstract representation of the topology of concurrently interacting entities, which allows us to encapsulate generic principles of reasoning about\n            <jats:italic>deadlock freedom<\/jats:italic>\n            . Connectivity graphs are\n            <jats:italic>parametric<\/jats:italic>\n            in their vertices (representing entities like threads and channels) and their edges (representing references between entities) with labels (representing interaction protocols). We prove deadlock and memory leak freedom in the style of progress and preservation and use\n            <jats:italic>separation logic<\/jats:italic>\n            as a meta theoretic tool to treat connectivity graph edges and labels substructurally. To prove preservation locally, we distill generic separation logic rules for\n            <jats:italic>local graph transformations<\/jats:italic>\n            that preserve acyclicity of the connectivity graph. To prove global progress locally, we introduce a\n            <jats:italic>waiting induction<\/jats:italic>\n            principle for acyclic connectivity graphs. We mechanize our results in Coq, and instantiate our method with a higher-order binary session-typed language to obtain the first mechanized proof of deadlock and leak freedom.\n          <\/jats:p>","DOI":"10.1145\/3498662","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-33","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Connectivity graphs: a method for proving deadlock freedom based on separation logic"],"prefix":"10.1145","volume":"6","author":[{"given":"Jules","family":"Jacobs","sequence":"first","affiliation":[{"name":"Radboud University Nijmegen, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephanie","family":"Balzer","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"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, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01531058"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110281"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2018.30"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_22"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022251"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_33"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_19"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.38.4"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454041"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45237-7_17"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.02.023"},{"key":"e_1_2_2_13_1","volume-title":"Ferrite: A Judgmental Embedding of Session Types in Rust. CoRR, abs\/2009.13619","author":"Chen Ruofei","year":"2020","unstructured":"Ruofei Chen and Stephanie Balzer . 2020 . Ferrite: A Judgmental Embedding of Session Types in Rust. CoRR, abs\/2009.13619 (2020), arxiv:2009.13619. arxiv:2009.13619 Ruofei Chen and Stephanie Balzer. 2020. Ferrite: A Judgmental Embedding of Session Types in Rust. CoRR, abs\/2009.13619 (2020), arxiv:2009.13619. arxiv:2009.13619"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3414080.3414109"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000188"},{"volume-title":"\u201cstandard library","author":"Team The","key":"e_1_2_2_16_1","unstructured":"The Coq-std++ Team . 2021. An extended \u201cstandard library \u201d for Coq . Available online at https:\/\/gitlab.mpi-sws.org\/iris\/stdpp The Coq-std++ Team. 2021. An extended \u201cstandard library\u201d for Coq. Available online at https:\/\/gitlab.mpi-sws.org\/iris\/stdpp"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.4501022"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS.2015.33"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-85315-0_8"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.15"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_5"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209146"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470654"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11785477_20"},{"key":"e_1_2_2_25_1","volume-title":"Separating Sessions Smoothly. CoRR, abs\/2105.08996","author":"Fowler Simon","year":"2021","unstructured":"Simon Fowler , Wen Kokke , Ornela Dardha , Sam Lindley , and J. Garrett Morris . 2021. Separating Sessions Smoothly. CoRR, abs\/2105.08996 ( 2021 ), arxiv:2105.08996. arxiv:2105.08996 Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, and J. Garrett Morris. 2021. Separating Sessions Smoothly. CoRR, abs\/2105.08996 (2021), arxiv:2105.08996. arxiv:2105.08996"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290341"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(3:7)2011"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.314.3"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990268"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129514000231"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_15"},{"key":"e_1_2_2_32_1","volume-title":"Practical Foundations for Programming Languages","author":"Harper Robert","unstructured":"Robert Harper . 2016. Practical Foundations for Programming Languages ( 2 nd ed.). Cambridge University Press . isbn:1107150302 https:\/\/doi.org\/10.5555\/3002812 Robert Harper. 2016. Practical Foundations for Programming Languages (2nd ed.). Cambridge University Press. isbn:1107150302 https:\/\/doi.org\/10.5555\/3002812","edition":"2"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371074"},{"key":"e_1_2_2_34_1","doi-asserted-by":"crossref","unstructured":"Jonas Kastberg Hinrichsen Jesper Bengtson and Robbert Krebbers. 2021. Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic. arxiv:2010.15030v1 Manuscript.  Jonas Kastberg Hinrichsen Jesper Bengtson and Robbert Krebbers. 2021. Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic. arxiv:2010.15030v1 Manuscript.","DOI":"10.46298\/lmcs-18(2:16)2022"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439914"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57208-2_35"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053567"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0032742"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360215"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(03)00325-6"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110282"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2018.08.005"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.69.6"},{"key":"e_1_2_2_45_1","doi-asserted-by":"crossref","unstructured":"Jules Jacobs Stephanie Balzer and Robbert Krebbers. 2021. Appendix and Coq mechanization of \u201cConnectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic\u201d. The most recent version is at https:\/\/github.com\/julesjacobs\/cgraphs  Jules Jacobs Stephanie Balzer and Robbert Krebbers. 2021. Appendix and Coq mechanization of \u201cConnectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic\u201d. The most recent version is at https:\/\/github.com\/julesjacobs\/cgraphs","DOI":"10.1145\/3498662"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2808098.2808100"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_10"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_14"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1997.614941"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2002.3171"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817949_16"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/330249.330251"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44618-4_35"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.304.4"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290337"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-02444-8_21"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_23"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976002.2976018"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951921"},{"key":"e_1_2_2_65_1","unstructured":"Sam Lindley and J. Garrett Morris. 2017. Lightweight Functional Session Types. In Behavioural Types: from Theory to Tools.  Sam Lindley and J. Garrett Morris. 2017. Lightweight Functional Session Types. In Behavioural Types: from Theory to Tools."},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.104.3"},{"key":"e_1_2_2_67_1","unstructured":"Fabrizio Montesi. 2021. Introduction to Choreographies. Accepted for publication by Cambridge University Press.  Fabrizio Montesi. 2021. Introduction to Choreographies. Accepted for publication by Cambridge University Press."},{"key":"e_1_2_2_68_1","volume-title":"abs\/1803.01049","author":"Montesi Fabrizio","year":"2018","unstructured":"Fabrizio Montesi and Marco Peressotti . 2018. Classical Transitions . CoRR , abs\/1803.01049 ( 2018 ), arxiv:1803.01049. arxiv:1803.01049 Fabrizio Montesi and Marco Peressotti. 2018. Classical Transitions. CoRR, abs\/1803.01049 (2018), arxiv:1803.01049. arxiv:1803.01049"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.211.7"},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000289"},{"key":"e_1_2_2_73_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.08.001"},{"key":"e_1_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_1"},{"key":"e_1_2_2_75_1","volume-title":"Types and Programming Languages","author":"Pierce Benjamin C.","year":"2091","unstructured":"Benjamin C. Pierce . 2002. Types and Programming Languages ( 1 st ed.). The MIT Press . isbn:026216 2091 https:\/\/doi.org\/10.5555\/509043 Benjamin C. Pierce. 2002. Types and Programming Languages (1st ed.). The MIT Press. isbn:0262162091 https:\/\/doi.org\/10.5555\/509043","edition":"1"},{"key":"e_1_2_2_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411286.1411290"},{"key":"e_1_2_2_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473567"},{"key":"e_1_2_2_79_1","unstructured":"Jason Reed. 2009. A Judgmental Deconstruction of Modal Logic. http:\/\/www.cs.cmu.edu\/~jcreed\/papers\/jdml.pdf Unpublished manuscript.  Jason Reed. 2009. A Judgmental Deconstruction of Modal Logic. http:\/\/www.cs.cmu.edu\/~jcreed\/papers\/jdml.pdf Unpublished manuscript."},{"key":"e_1_2_2_80_1","doi-asserted-by":"crossref","unstructured":"Pedro Rocha and Lu\u00eds Caires. 2021. Propositions-as-Types and Shared State. NOVA LINCS.  Pedro Rocha and Lu\u00eds Caires. 2021. Propositions-as-Types and Shared State. NOVA LINCS.","DOI":"10.1145\/3473584"},{"key":"e_1_2_2_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434303"},{"key":"e_1_2_2_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373818"},{"key":"e_1_2_2_83_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2016.21"},{"key":"e_1_2_2_84_1","doi-asserted-by":"publisher","DOI":"10.6092\/issn.1972-5787\/1574"},{"key":"e_1_2_2_85_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_34"},{"key":"e_1_2_2_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/3354166.3354184"},{"key":"e_1_2_2_88_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_20"},{"key":"e_1_2_2_89_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.05.002"},{"key":"e_1_2_2_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364568"},{"key":"e_1_2_2_91_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_2_2_92_1","doi-asserted-by":"publisher","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\/3498662","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498662","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498662","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:27Z","timestamp":1750188627000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498662"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":90,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498662"],"URL":"https:\/\/doi.org\/10.1145\/3498662","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}