{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:32:26Z","timestamp":1767929546498,"version":"3.49.0"},"reference-count":31,"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\/100008398","name":"VILLUM Foundation","doi-asserted-by":"crossref","award":["25804"],"award-info":[{"award-number":["25804"]}],"id":[{"id":"10.13039\/100008398","id-type":"DOI","asserted-by":"crossref"}]}],"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            A program is said to be well-bracketed if every called function must return before its caller can resume execution. This is often the case. Well-bracketedness has been captured semantically as a condition on strategies in fully abstract games models and multiple prior works have studied well-bracketedness by showing correctness\/security properties of programs where such properties depend on the well-bracketed nature of control flow. The latter category of prior works have all used involved relational models with explicit state-transition systems capturing the relevant parts of the control flow of the program. In this paper we present the first Hoare-style\n            <jats:italic toggle=\"yes\">program logic<\/jats:italic>\n            based on separation logic for reasoning about well-bracketedness and use it to show correctness of well-bracketed programs both directly and also through defining unary and binary logical relations models based on this program logic. All results presented in this paper are formalized on top of the Iris framework and mechanized in the Coq proof assistant.\n          <\/jats:p>","DOI":"10.1145\/3632862","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"575-603","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["The Logical Essence of Well-Bracketed Control Flow"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2237-851X","authenticated-orcid":false,"given":"Amin","family":"Timany","sequence":"first","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3072-4045","authenticated-orcid":false,"given":"Arma\u00ebl","family":"Gu\u00e9neau","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Saclay - CNRS - ENS Paris-Saclay - Inria - Laboratoire M\u00e9thodes Formelles, Gif-sur-Yvette, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1320-0098","authenticated-orcid":false,"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"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.1109\/LICS.1998.705669"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480925"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17127-8_6"},{"key":"e_1_3_1_5_1","unstructured":"Lars Birkedal and Ale\u0161 Bizjak. 2017. Lecture Notes on Iris: Higher-Order Concurrent Separation Log. (2017). http:\/\/irisproject.org\/tutorial-pdfs\/iris-lecture-notes.pdf"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473586"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434314"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863566"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434287"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103666"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2917"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470524"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02059-9_3"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","unstructured":"J. Laird. 1997. Full abstraction for functional languages with control. In Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science. 58\u201367. https:\/\/doi.org\/10.1109\/LICS.1997.614931 10.1109\/LICS.1997.614931","DOI":"10.1109\/LICS.1997.614931"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73420-8_58"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74915-8_23"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","unstructured":"Soren B. Lassen and Paul Blain Levy. 2008. Typed Normal Form Bisimulation for Parametric Polymorphism. In 2008 23rd Annual IEEE Symposium on Logic in Computer Science. 341\u2013352. https:\/\/doi.org\/10.1109\/LICS.2008.26 10.1109\/LICS.2008.26","DOI":"10.1109\/LICS.2008.26"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.12.036"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","unstructured":"Andrzej S. Murawski and Nikos Tzevelekos. 2011. Game Semantics for Good General References. In 2011 IEEE 26th Annual Symposium on Logic in Computer Science. 75\u201384. https:\/\/doi.org\/10.1109\/LICS.2011.31 10.1109\/LICS.2011.31","DOI":"10.1109\/LICS.2011.31"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_16"},{"key":"e_1_3_1_23_1","first-page":"227","volume-title":"Operational Reasoning for Functions with Local State.","author":"Pitts A. M.","year":"1999","unstructured":"A. M. Pitts and I. D. B. Stark. 1999. Operational Reasoning for Functions with Local State. Cambridge University Press, USA, 227\u2013274."},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","unstructured":"Francois Pottier. 2008. Hiding Local State in Direct Style: A Higher-Order Anti-Frame Rule. In 2008 23rd Annual IEEE Symposium on Logic in Computer Science. 331\u2013340. https:\/\/doi.org\/10.1109\/LICS.2008.16 10.1109\/LICS.2008.16","DOI":"10.1109\/LICS.2008.16"},{"key":"e_1_3_1_25_1","unstructured":"Fran\u00e7ois Pottier. 2009. Generalizing the higher-order frame and anti-frame rules. (2009). http:\/\/cambium.inria.fr\/~fpottier\/publis\/fpottier-gaf-2009.pdf [Unpublished notes available on Pottier\u2019s institutional homepage (accessed on Jun 7th 2023)]."},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290332"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04164-8_17"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04027-6_33"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964015"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341709"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439931"},{"key":"e_1_3_1_32_1","unstructured":"Amin Timany Robbert Krebbers Derek Dreyer and Lars Birkedal. 2022. A Logical Approach to Type Soundness. Reported under submission on https:\/\/iris-project.org\/ (2022). https:\/\/iris-project.org\/pdfs\/2022-submitted-logical-type-soundness.pdf"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632862","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632862","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:03:17Z","timestamp":1751659397000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632862"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":31,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632862"],"URL":"https:\/\/doi.org\/10.1145\/3632862","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"}}]}}