{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:16Z","timestamp":1780994716154,"version":"3.54.1"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2019,7,26]],"date-time":"2019-07-26T00:00:00Z","timestamp":1564099200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,7,26]]},"abstract":"<jats:p>\n            Concurrent higher-order imperative programming languages with continuations are very flexible and allow for the implementation of sophisticated programming patterns. For instance, it is well known that continuations can be used to implement cooperative concurrency. Continuations can also simplify web server implementations. This, in particular, helps simplify keeping track of the state of server\u2019s clients. However, such advanced programming languages are very challenging to reason about. One of the main challenges in reasoning about programs in the presence of continuations is due to the fact that the non-local flow of control breaks the\n            <jats:italic>bind<\/jats:italic>\n            rule, one of the important modular reasoning principles of Hoare logic.\n          <\/jats:p>\n          <jats:p>In this paper we present the first completely formalized tool for interactive mechanized relational verification of programs written in a concurrent higher-order imperative programming language with continuations (call\/cc and throw). We develop novel logical relations which can be used to give mechanized proofs of relational properties. In particular, we prove correctness of an implementation of cooperative concurrency with continuations. In addition, we show that that a rudimentary web server implemented using the continuation-based pattern is contextually equivalent to one implemented without the continuation-based pattern. We introduce context-local reasoning principles for our calculus which allows us to regain modular reasoning principles for the fragment of the language without non-local control flow. These novel reasoning principles can be used in tandem with our (non-context-local) Hoare logic for reasoning about programs that do feature non-local control flow. Indeed, we use the combination of context-local and non-context-local reasoning to simplify reasoning about the examples.<\/jats:p>","DOI":"10.1145\/3341709","type":"journal-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:55:51Z","timestamp":1564433751000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["Mechanized relational verification of concurrent programs with continuations"],"prefix":"10.1145","volume":"3","author":[{"given":"Amin","family":"Timany","sequence":"first","affiliation":[{"name":"KU Leuven, Belgium"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,7,26]]},"reference":[{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664579"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11623-0_11"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926401"},{"key":"e_1_2_2_7_1","unstructured":"Lars Birkedal Filip Sieczkowski and Jacob Thamsborg. 2012. A Concurrent Logical Relation. In CSL.  Lars Birkedal Filip Sieczkowski and Jacob Thamsborg. 2012. A Concurrent Logical Relation. In CSL."},{"key":"e_1_2_2_8_1","doi-asserted-by":"crossref","unstructured":"Andrea Cerone Alexey Gotsman and Hongseok Yang. 2014. Parameterised Linearisability. In ICALP.  Andrea Cerone Alexey Gotsman and Hongseok Yang. 2014. Parameterised Linearisability. In ICALP.","DOI":"10.1007\/978-3-662-43951-7_9"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.01.004"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91622"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544174.2500593"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_2_2_14_1","doi-asserted-by":"crossref","unstructured":"T. Dinsdale-Young M. Dodds P. Gardner M. Parkinson and V. Vafeiadis. 2010. Concurrent abstract predicates. In ECOOP. 504\u2013528.   T. Dinsdale-Young M. Dodds P. Gardner M. Parkinson and V. Vafeiadis. 2010. Concurrent abstract predicates. In ECOOP. 504\u2013528.","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_2_2_15_1","doi-asserted-by":"crossref","unstructured":"D. Dreyer A. Ahmed and L. Birkedal. 2011. Logical Step-Indexed Logical Relations. LMCS 7 2:16 (2011).  D. Dreyer A. Ahmed and L. Birkedal. 2011. Logical Step-Indexed Logical Relations. LMCS 7 2:16 (2011).","DOI":"10.2168\/LMCS-7(2:16)2011"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681200024X"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73576"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"e_1_2_2_19_1","volume-title":"More: Systems Programming with Racket. https:\/\/docs.racket-lang.org\/more\/index.html .","author":"Flatt Matthew","year":"2017"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/318593.318654"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/800055.802046"},{"key":"e_1_2_2_22_1","unstructured":"Greg Hendershott. 2017. http:\/\/www.greghendershott.com\/2014\/09\/written-in-racket.html .  Greg Hendershott. 2017. http:\/\/www.greghendershott.com\/2014\/09\/written-in-racket.html ."},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9008-y"},{"key":"e_1_2_2_30_1","unstructured":"Morten Krogh-Jespersen Kasper Svendsen and Lars Birkedal. 2017. A Logical Account of a Type-and-Effect System. In POPL.  Morten Krogh-Jespersen Kasper Svendsen and Lars Birkedal. 2017. A Logical Account of a Type-and-Effect System. In POPL."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/788019.788859"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429134"},{"key":"e_1_2_2_33_1","unstructured":"Matt Might. 2017. http:\/\/matt.might.net\/articles\/low-level-web-in-racket\/ .  Matt Might. 2017. http:\/\/matt.might.net\/articles\/low-level-web-in-racket\/ ."},{"key":"e_1_2_2_34_1","volume-title":"Higher-Order Linearisability. In CONCUR","author":"Andrzej","year":"2017"},{"key":"e_1_2_2_35_1","doi-asserted-by":"crossref","unstructured":"Keiko Nakata and Andri Saar. 2013. Compiling Cooperative Task Management to Continuations. In Fundamentals of Software Engineering Farhad Arbab and Marjan Sirjani (Eds.).  Keiko Nakata and Andri Saar. 2013. Compiling Cooperative Task Management to Continuations. In Fundamentals of Software Engineering Farhad Arbab and Marjan Sirjani (Eds.).","DOI":"10.1007\/978-3-642-40213-5_7"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_16"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_2_38_1","volume-title":"Advanced Topics in Types and Programming Languages","author":"Pitts Andrew M."},{"key":"e_1_2_2_39_1","volume-title":"LCF considered as a programming language. Theoretical computer science 5, 3","author":"Plotkin Gordon D.","year":"1977"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-004-4866-z"},{"key":"e_1_2_2_41_1","first-page":"359","article-title":"Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions","volume":"9236","author":"Sch\u00e4fer Steven","year":"2015","journal-title":"ITP (LNCS)"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737964"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190244"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158152"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429111"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341709","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341709","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:24Z","timestamp":1750207404000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341709"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,26]]},"references-count":46,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2019,7,26]]}},"alternative-id":["10.1145\/3341709"],"URL":"https:\/\/doi.org\/10.1145\/3341709","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,7,26]]},"assertion":[{"value":"2019-07-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}