{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:43:36Z","timestamp":1770291816599,"version":"3.49.0"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T00:00:00Z","timestamp":1728345600000},"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":[[2024,10,8]]},"abstract":"<jats:p>\n                    Type systems and program logics based on session types provide powerful high-level reasoning principles for message-passing concurrency. Modern versions employ bidirectional session channels that (1) are asynchronous so that\n                    <jats:bold>\n                      <jats:monospace>send<\/jats:monospace>\n                    <\/jats:bold>\n                    operations do not block, (2) have buffers in both directions so that both parties can send messages in parallel, and (3) feature a\n                    <jats:monospace>\n                      <jats:bold>link<\/jats:bold>\n                    <\/jats:monospace>\n                    operation (also called\n                    <jats:monospace>\n                      <jats:bold>forward<\/jats:bold>\n                    <\/jats:monospace>\n                    ) to concisely write programs in\n                    <jats:italic toggle=\"yes\">process style<\/jats:italic>\n                    . These features complicate a low-level lock-free implementation of channels and therefore increase the gap between the meta theory of prior work\u2014which is verified w.r.t. a high-level semantics of channels (\n                    <jats:italic toggle=\"yes\">e.g<\/jats:italic>\n                    .,\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mi>\u03c0<\/mml:mi>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    -calculus)\u2014and the code that runs on an actual computer.\n                  <\/jats:p>\n                  <jats:p>\n                    We address this problem by verifying a low-level lock-free implementation of session channels w.r.t. a high-level specification based on session types. We carry out our verification in a layered manner by employing the Iris framework for concurrent separation logic. We start with an abstract specification of (unidirectional) queues\u2014of which we provide a linked-list and array-segment based implementation\u2014and gradually build up to session channels with all of the aforementioned features. To make a layered verification possible we develop two logical abstractions\u2014\n                    <jats:italic toggle=\"yes\">queues with ghost linking and pairing invariants<\/jats:italic>\n                    \u2014to reason about the atomicity and changing endpoints due to linking, respectively. All our results are mechanized in the Coq proof assistant.\n                  <\/jats:p>","DOI":"10.1145\/3689732","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T03:23:04Z","timestamp":1728357784000},"page":"588-617","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Verified Lock-Free Session Channels with Linking"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-8101-5647","authenticated-orcid":false,"given":"Thomas","family":"Somers","sequence":"first","affiliation":[{"name":"Radboud University Nijmegen, Nijmegen, Netherlands"}],"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,10,8]]},"reference":[{"key":"e_1_3_1_2_2","unstructured":"Amal Ahmed. 2004. Semantics of Types for Mutable State. Ph. D. Dissertation. Princeton University."},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(89)90027-5"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","unstructured":"Andrew W. Appel and David A. McAllester. 2001. An indexed model of recursive types for foundational proof-carrying code. TOPLAS 23 5 (2001) 657\u2013683. https:\/\/doi.org\/10.1145\/504709.504712 10.1145\/504709.504712","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_1_5_2","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 Martin Hofmann and Matthias Felleisen (Eds.). 109\u2013122. https:\/\/doi.org\/10.1145\/1190216.1190235 10.1145\/1190216.1190235","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","unstructured":"Lars Birkedal Kristian St\u00f8vring and Jacob Thamsborg. 2010. The category-theoretic solution of recursive metric-space equations. TCS 411 47 (2010) 4102\u20134122. 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_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290378"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","unstructured":"John Boyland. 2003. Checking Interference with Fractional Permissions. In SAS (LNCS Vol. 2694). 55\u201372. https:\/\/doi.org\/10.1007\/3-540-44898-5_4 10.1007\/3-540-44898-5_4","DOI":"10.1007\/3-540-44898-5_4"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","unstructured":"Stephen Brookes. 2007. A semantics for concurrent separation logic. TCS 375 1-3 (2007) 227\u2013270. https:\/\/doi.org\/10.1016\/J.TCS.2006.12.034 10.1016\/J.TCS.2006.12.034","DOI":"10.1016\/J.TCS.2006.12.034"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","unstructured":"Lu\u00eds Caires and Frank Pfenning. 2010. Session Types as Intuitionistic Linear Propositions. In CONCUR (LNCS Vol. 6269). 222\u2013236. 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_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-018-9457-5"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","unstructured":"Quentin Carbonneaux Noam Zilberstein Christoph Klee Peter W. O\u2019Hearn and Francesco Zappa Nardelli. 2022. Applying formal verification to microkernel IPC at Meta. In CPP. 116\u2013129. https:\/\/doi.org\/10.1145\/3497775.3503681 10.1145\/3497775.3503681","DOI":"10.1145\/3497775.3503681"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","unstructured":"Pedro da Rocha Pinto Thomas Dinsdale-Young and Philippa Gardner. 2014. TaDA: A Logic for Time and Data Abstraction. In ECOOP (LNCS Vol. 8586). 207\u2013231. https:\/\/doi.org\/10.1007\/978-3-662-44202-9_9 10.1007\/978-3-662-44202-9_9","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","unstructured":"Hoang-Hai Dang Jaehwang Jung Jaemin Choi Duc-Than Nguyen William Mansky Jeehoon Kang and Derek Dreyer. 2022. Compass: strong and compositional library specifications in relaxed memory separation logic. In PLDI. 792\u2013808. https:\/\/doi.org\/10.1145\/3519939.3523451 10.1145\/3519939.3523451","DOI":"10.1145\/3519939.3523451"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-18(1:9)2022"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","unstructured":"Ivana Filipovic Peter W. O\u2019Hearn Noam Rinetzky and Hongseok Yang. 2009. Abstraction for Concurrent Objects. In ESOP (LNCS Vol. 5502). 252\u2013266. https:\/\/doi.org\/10.1007\/978-3-642-00590-9_19 10.1007\/978-3-642-00590-9_19","DOI":"10.1007\/978-3-642-00590-9_19"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-19(3:3)2023"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990268"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3607859"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","unstructured":"Maurice Herlihy and Jeannette M. Wing. 1990. Linearizability: A Correctness Condition for Concurrent Objects. TOPLAS 12 3 (1990) 463\u2013492. https:\/\/doi.org\/10.1145\/78969.78972 10.1145\/78969.78972","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","unstructured":"Jonas Kastberg Hinrichsen Jesper Bengtson and Robbert Krebbers. 2020. Actris: session-type based reasoning in separation logic. PACMPL 4 POPL (2020) 6:1\u20136:30. https:\/\/doi.org\/10.1145\/3371074 10.1145\/3371074","DOI":"10.1145\/3371074"},{"key":"e_1_3_1_22_2","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 18 2 (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_23_2","doi-asserted-by":"publisher","unstructured":"Jonas Kastberg Hinrichsen Jules Jacobs and Robbert Krebbers. 2024. Multris: Functional Verification of Multiparty Message Passing in Separation Logic. PACMPL 8 OOPSLA (2024) 322:1\u2013322:29. https:\/\/doi.org\/10.1145\/3689762 10.1145\/3689762","DOI":"10.1145\/3689762"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","unstructured":"Jonas Kastberg Hinrichsen Dani\u00ebl Louwrink Robbert Krebbers and Jesper Bengtson. 2021. Machine-checked semantic session typing. In CPP. 178\u2013198. https:\/\/doi.org\/10.1145\/3437992.3439914 10.1145\/3437992.3439914","DOI":"10.1145\/3437992.3439914"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","unstructured":"Kohei Honda. 1993. Types for Dyadic Interaction. In CONCUR (LNCS Vol. 715). 509\u2013523. 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_26_2","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 (LNCS Vol. 1381). 122\u2013138. https:\/\/doi.org\/10.1007\/BFB0053567 10.1007\/BFB0053567","DOI":"10.1007\/BFB0053567"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","unstructured":"Kohei Honda Nobuko Yoshida and Marco Carbone. 2008. Multiparty asynchronous session types. In POPL. 273\u2013284. https:\/\/doi.org\/10.1145\/1328438.1328472 10.1145\/1328438.1328472","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_3_1_28_2","unstructured":"Iris Development Team. 2024. The Coq mechanization of Iris. https:\/\/gitlab.mpi-sws.org\/iris\/iris\/"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","unstructured":"Bart Jacobs and Frank Piessens. 2011. Expressive modular fine-grained concurrency specification. In POPL. 271\u2013282. https:\/\/doi.org\/10.1145\/1926385.1926417 10.1145\/1926385.1926417","DOI":"10.1145\/1926385.1926417"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632889"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Lars Birkedal and Derek Dreyer. 2016. Higher-order ghost state. In ICFP. 256\u2013269. https:\/\/doi.org\/10.1145\/2951913.2951943 10.1145\/2951913.2951943","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ales Bizjak Lars Birkedal and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. JFP 28 (2018) e20. https:\/\/doi.org\/10.1017\/S0956796818000151 10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_33_2","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. 637\u2013650. https:\/\/doi.org\/10.1145\/2676726.2676980 10.1145\/2676726.2676980","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_1_34_2","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. PACMPL 2 ICFP (2018) 77:1\u201377:30. https:\/\/doi.org\/10.1145\/3236772 10.1145\/3236772","DOI":"10.1145\/3236772"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Ralf Jung Ales Bizjak Jacques-Henri Jourdan Derek Dreyer and Lars Birkedal. 2017. The Essence of Higher-Order Concurrent Separation Logic. In ESOP (LNCS Vol. 10201). 696\u2013723. 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_36_2","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Amin Timany and Lars Birkedal. 2017. Interactive proofs in higher-order concurrent separation logic. In POPL. 205\u2013217. https:\/\/doi.org\/10.1145\/3009837.3009855 10.1145\/3009837.3009855","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","unstructured":"Morten Krogh-Jespersen Amin Timany Marit Edna Ohlenbusch Simon Oddershede Gregersen and Lars Birkedal. 2020. Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems. In ESOP (LNCS Vol. 12075). 336\u2013365. https:\/\/doi.org\/10.1007\/978-3-030-44914-8_13 10.1007\/978-3-030-44914-8_13","DOI":"10.1007\/978-3-030-44914-8_13"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","unstructured":"Hongjin Liang and Xinyu Feng. 2013. Modular verification of linearizability with non-fixed linearization points. In PLDI. 459\u2013470. https:\/\/doi.org\/10.1145\/2491956.2462189 10.1145\/2491956.2462189","DOI":"10.1145\/2491956.2462189"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","unstructured":"Sam Lindley and J. Garrett Morris. 2015. A Semantics for Propositions as Sessions. In ESOP (LNCS Vol. 9032). 560\u2013584. 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_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133911"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","unstructured":"Glen M\u00e9vel and Jacques-Henri Jourdan. 2021. Formal verification of a concurrent bounded queue in a weak memory model. PACMPL 5 ICFP (2021) 1\u201329. https:\/\/doi.org\/10.1145\/3473571 10.1145\/3473571","DOI":"10.1145\/3473571"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","unstructured":"Glen M\u00e9vel Jacques-Henri Jourdan and Fran\u00e7ois Pottier. 2019. Time Credits and Time Receipts in Iris. In ESOP (LNCS Vol. 11423). 3\u201329. https:\/\/doi.org\/10.1007\/978-3-030-17184-1_1 10.1007\/978-3-030-17184-1_1","DOI":"10.1007\/978-3-030-17184-1_1"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2015.02.002"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","unstructured":"Dimitris Mostrous Nobuko Yoshida and Kohei Honda. 2009. Global Principal Typing in Partially Commutative Asynchronous Sessions. In ESOP (LNCS Vol. 5502). 316\u2013332. https:\/\/doi.org\/10.1007\/978-3-642-00590-9_23 10.1007\/978-3-642-00590-9_23","DOI":"10.1007\/978-3-642-00590-9_23"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","unstructured":"Hiroshi Nakano. 2000. A Modality for Recursion. In LICS. 255\u2013266. https:\/\/doi.org\/10.1109\/LICS.2000.855774 10.1109\/LICS.2000.855774","DOI":"10.1109\/LICS.2000.855774"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","unstructured":"Peter W. O\u2019Hearn. 2007. Resources concurrency and local reasoning. TCS 375 1\u20133 (2007) 271-307. https:\/\/doi.org\/10.1016\/J.TCS.2006.12.035 10.1016\/J.TCS.2006.12.035","DOI":"10.1016\/J.TCS.2006.12.035"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","unstructured":"Peter W. O\u2019Hearn8 John C. Reynolds and Hongseok Yang. 2001. Local Reasoning about Programs that Alter Data Structures. In CSL (LNCS Vol. 2142). 1\u201319. 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_49_2","doi-asserted-by":"publisher","unstructured":"Sunho Park Jaewoo Kim Ike Mulder Jaehwang Jung Janggun Lee Robbert Krebbers and Jeehoon Kang. 2024. A Proof Recipe for Linearizability in Relaxed Memory Separation Logic. PACMPL 8 PLDI (2024). https:\/\/doi.org\/10.1145\/3656384 10.1145\/3656384","DOI":"10.1145\/3656384"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","unstructured":"John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS. 55\u201374. https:\/\/doi.org\/10.1109\/LICS.2002.1029817 10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_1_51_2","doi-asserted-by":"publisher","unstructured":"Pedro Rocha and Lu\u00eds Caires. 2023. Safe Session-Based Concurrency with Shared Linear State. In ESOP (LNCS Vol. 13990). 421\u2013450. 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_52_2","doi-asserted-by":"publisher","unstructured":"Thomas Somers and Robbert Krebbers. 2024. Artifact of \u2019Verified Lock-Free Session Channels with Linking\u2019. https:\/\/doi.org\/10.5281\/zenodo.13599952 10.5281\/zenodo.13599952","DOI":"10.5281\/zenodo.13599952"},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","unstructured":"Matthieu Sozeau and Nicolas Oury. 2008. First-Class Type Classes. In TPHOLs (LNCS Vol. 5170). 278\u2013293. https:\/\/doi.org\/10.1007\/978-3-540-71067-7_23 10.1007\/978-3-540-71067-7_23","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","unstructured":"Simon Spies Lennard G\u00e4her Joseph Tassarotti Ralf Jung Robbert Krebbers Lars Birkedal and Derek Dreyer. 2022. Later credits: resourceful reasoning for the later modality. PACMPL 6 ICFP (2022) 283\u2013311. https:\/\/doi.org\/10.1145\/3547631 10.1145\/3547631","DOI":"10.1145\/3547631"},{"key":"e_1_3_1_55_2","doi-asserted-by":"publisher","unstructured":"Kasper Svendsen Lars Birkedal and Matthew J. Parkinson. 2013. Modular Reasoning about Separation of Concurrent Data Structures. In ESOP (LNCS Vol. 7792). 169\u2013188. https:\/\/doi.org\/10.1007\/978-3-642-37036-6_11 10.1007\/978-3-642-37036-6_11","DOI":"10.1007\/978-3-642-37036-6_11"},{"key":"e_1_3_1_56_2","doi-asserted-by":"publisher","unstructured":"Joseph Tassarotti Ralf Jung and Robert Harper. 2017. A Higher-Order Logic for Concurrent Termination-Preserving Refinement. In ESOP (LNCS Vol. 10201). 909\u2013936. 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_57_2","doi-asserted-by":"crossref","unstructured":"Amin Timany Robbert Krebbers Derek Dreyer and Lars Birkedal. 2024. A Logical Approach to Type Soundness. To appear in Journal of the ACM (JACM).","DOI":"10.1145\/3676954"},{"key":"e_1_3_1_58_2","doi-asserted-by":"publisher","unstructured":"Bernardo Toninho Lu\u00eds Caires and Frank Pfenning. 2011. Dependent session types via intuitionistic linear type theory. In PPDP (Odense Denmark). 161\u2013172. https:\/\/doi.org\/10.1145\/2003476.2003499 10.1145\/2003476.2003499","DOI":"10.1145\/2003476.2003499"},{"key":"e_1_3_1_59_2","doi-asserted-by":"publisher","unstructured":"Simon Friis Vindum and Lars Birkedal. 2021. Contextual refinement of the Michael\u2013Scott queue (proof pearl). In CPP. 76\u201390. https:\/\/doi.org\/10.1145\/3437992.3439930 10.1145\/3437992.3439930","DOI":"10.1145\/3437992.3439930"},{"key":"e_1_3_1_60_2","doi-asserted-by":"publisher","unstructured":"Simon Friis Vindum Dan Frumin and Lars Birkedal. 2022. Mechanized verification of a fine-grained concurrent queue from Meta\u2019s Folly library. In CPP. 100\u2013115. https:\/\/doi.org\/10.1145\/3497775.3503689 10.1145\/3497775.3503689","DOI":"10.1145\/3497775.3503689"},{"key":"e_1_3_1_61_2","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681400001X"},{"key":"e_1_3_1_62_2","doi-asserted-by":"publisher","unstructured":"Max Willsey Rokhini Prabhu and Frank Pfenning. 2016. Design and Implementation of Concurrent C0. In LINEARITY (EPTCS Vol. 238). 73\u201382. https:\/\/doi.org\/10.4204\/EPTCS.238.8 10.4204\/EPTCS.238.8","DOI":"10.4204\/EPTCS.238.8"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689732","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689732","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T09:07:08Z","timestamp":1770196028000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689732"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":61,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2024,10,8]]}},"alternative-id":["10.1145\/3689732"],"URL":"https:\/\/doi.org\/10.1145\/3689732","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"assertion":[{"value":"2024-04-06","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}