{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:13:16Z","timestamp":1775790796732,"version":"3.50.1"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"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":[[2025,1,7]]},"abstract":"<jats:p>\n                    Program logics have proven a successful strategy for verification of complex programs. By providing local reasoning and means of abstraction and composition, they allow reasoning principles for individual components of a program to be combined to prove guarantees about a whole program. Crucially, these components and their proofs can be\n                    <jats:italic toggle=\"yes\">reused<\/jats:italic>\n                    . However, this reuse is only available once the program logic has been defined. It is a frustrating fact of the status quo that whoever defines a new program logic must establish every part, both semantics and proof rules, from scratch. In spite of programming languages and program logics typically sharing many core features, reuse is generally not available across languages. Even inside one language, if the same underlying operation appears in multiple language primitives, reuse is typically not possible when establishing proof rules for the program logic.\n                  <\/jats:p>\n                  <jats:p>\n                    To enable reuse across and inside languages when defining complex program logics (and proving them sound), we serve program logics\n                    <jats:italic toggle=\"yes\">\u00e0 la carte<\/jats:italic>\n                    by combining program logic fragments for the various effects of the language. Among other language features, the menu includes shared state, concurrency, and non-determinism as reusable, composable blocks that can be combined to define a program logic modularly. Our theory builds on ITrees as a framework to express language semantics and Iris as the underlying separation logic; the work has been mechanized in the Coq proof assistant.\n                  <\/jats:p>","DOI":"10.1145\/3704847","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"300-331","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Program Logics \u00e0 la Carte"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-6739-4890","authenticated-orcid":false,"given":"Max","family":"Vistrup","sequence":"first","affiliation":[{"name":"ETH Zurich, Z\u00fcrich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4591-743X","authenticated-orcid":false,"given":"Michael","family":"Sammler","sequence":"additional","affiliation":[{"name":"ETH Zurich, Z\u00fcrich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7669-6348","authenticated-orcid":false,"given":"Ralf","family":"Jung","sequence":"additional","affiliation":[{"name":"ETH Zurich, Z\u00fcrich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009878"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.8"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_14"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706339"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.30"},{"key":"e_1_3_2_7_2","first-page":"423","volume-title":"15th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2021, July 14-16, 2021","author":"Chajed Tej","year":"2021","unstructured":"Tej Chajed, Joseph Tassarotti, Mark Theng, Ralf Jung, M. Frans Kaashoek, and Nickolai Zeldovich. 2021.GoJournal: a verified, concurrent, crash-safe journaling system. In 15th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2021, July 14-16, 2021, Angela Demke Brown and Jay R. Lorch (Eds.). USENIX Association, 423\u2013439. https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/chajed"},{"key":"e_1_3_2_8_2","first-page":"1770","article-title":"Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq","volume":"7","author":"Chappe Nicolas","year":"2023","unstructured":"Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, and Steve Zdancewic. 2023.Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq. PACMPL 7, POPL (2023), 1770\u20131800. https:\/\/doi.org\/10.1145\/3571254 10.1145\/3571254","journal-title":"PACMPL"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3579834"},{"key":"e_1_3_2_10_2","volume-title":"USENIX Annual Technical Conference","author":"Chen Haogang","year":"2016","unstructured":"Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. 2016.Using Crash Hoare Logic for Certifying the FSCQ File System. In USENIX Annual Technical Conference. USENIX Association. https:\/\/www.usenix.org\/conference\/atc16\/technical-sessions\/presentation\/chen_haogang"},{"key":"e_1_3_2_11_2","unstructured":"Santiago Cuellar Nick Giannarakis Jean-Marie Madiot William Mansky Lennart Beringer Qinxiang Cao and Andrew W. Appel. 2020.Compiler correctness for concurrency: from concurrent separation logic to shared-memory assembly language. https:\/\/www.cs.princeton.edu\/~appel\/papers\/ccc.pdf"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/321420.321422"},{"key":"e_1_3_2_14_2","first-page":"332","article-title":"Modular Denotational Semantics for Effects with Guarded Interaction Trees","volume":"8","author":"Frumin Dan","year":"2024","unstructured":"Dan Frumin, Amin Timany, and Lars Birkedal. 2024.Modular Denotational Semantics for Effects with Guarded Interaction Trees. PACMPL 8, POPL (2024), 332\u2013361. https:\/\/doi.org\/10.1145\/3632854 10.1145\/3632854","journal-title":"PACMPL"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_27"},{"key":"e_1_3_2_16_2","unstructured":"Jason Gross. 2024. Answer to \u2018Is CoInductive \u201cextensionality\u201d sound in Coq? Is it generalizable?'. https:\/\/stackoverflow.com\/a\/69905520. Accessed: 2024-1024."},{"key":"e_1_3_2_17_2","first-page":"716","article-title":"Melocoton: A Program Logic for Verified Interoperability Between OCaml and C","volume":"7","author":"Gu\u00e9neau Arma\u00ebl","year":"2023","unstructured":"Arma\u00ebl Gu\u00e9neau, Johannes Hostert, Simon Spies, Michael Sammler, Lars Birkedal, and Derek Dreyer. 2023. Melocoton: A Program Logic for Verified Interoperability Between OCaml and C. PACMPL 7, OOPSLA2 (2023), 716\u2013744. https:\/\/doi.org\/10.1145\/3622823 10.1145\/3622823","journal-title":"PACMPL"},{"key":"e_1_3_2_18_2","first-page":"353","article-title":"Oracle Semantics for Concurrent Separation Logic","author":"Hobor Aquinas","year":"2008","unstructured":"Aquinas Hobor, Andrew W. Appel, and Francesco Zappa Nardelli. 2008. Oracle Semantics for Concurrent Separation Logic. In ESOP (LNCS, Vol. 4960). 353\u2013367. https:\/\/doi.org\/10.1007\/978-3-540-78739-6_27 10.1007\/978-3-540-78739-6_27","journal-title":"ESOP (LNCS, Vol. 4960)"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.03.020"},{"key":"e_1_3_2_20_2","first-page":"1385","article-title":"Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing","volume":"8","author":"Jacobs Jules","year":"2024","unstructured":"Jules Jacobs, Jonas Kastberg Hinrichsen, and Robbert Krebbers. 2024. Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing. PACMPL 8, POPL (2024), 1385\u20131417. https:\/\/doi.org\/10.1145\/3632889 10.1145\/3632889","journal-title":"PACMPL"},{"key":"e_1_3_2_21_2","first-page":"66:1","article-title":"Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing","volume":"2","author":"Jung Ralf","year":"2024","unstructured":"Ralf Jung, Jonas Kastberg Hinrichsen, and Robbert Krebbers. 2024. Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing. PACMPL 2, POPL (2018), 66:1\u201366:34. https:\/\/doi.org\/10.1145\/3158154 10.1145\/3158154","journal-title":"PACMPL"},{"key":"e_1_3_2_22_2","article-title":"Iris from the ground up: A modular foundation for higher-order concurrent separation logic","volume":"28","author":"Jung Ralf","year":"2018","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. F. Funct. Program. 28 (2018), e20. https:\/\/doi.org\/10.1017\/S0956796818000151 10.1017\/S0956796818000151","journal-title":"F. Funct. Program"},{"key":"e_1_3_2_23_2","first-page":"45:1","article-title":"The future is ours: Prophecy variables in separation logic","volume":"4","author":"Jung Ralf","year":"2020","unstructured":"Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs. 2020. The future is ours: Prophecy variables in separation logic. PACMPL 4, POPL (2020), 45:1\u201345:32. https:\/\/doi.org\/10.1145\/3371113 10.1145\/3371113","journal-title":"PACMPL"},{"key":"e_1_3_2_24_2","first-page":"77:1","article-title":"MoSeL: A general, extensible modal framework for interactive proofs in separation logic","volume":"2","author":"Krebbers Robbert","year":"2018","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","journal-title":"PACMPL"},{"key":"e_1_3_2_25_2","first-page":"696","article-title":"The Essence of Higher-Order Concurrent Separation Logic","author":"Krebbers Robbert","year":"2017","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","journal-title":"ESOP (LNCS, Vol. 10201)"},{"key":"e_1_3_2_26_2","first-page":"205","article-title":"Interactive proofs in higher-order concurrent separation logic","author":"Krebbers Robbert","year":"2017","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","journal-title":"POPL"},{"key":"e_1_3_2_27_2","first-page":"104:1","article-title":"Dijkstra monads for all","volume":"3","author":"Maillard Kenji","year":"2019","unstructured":"Kenji Maillard, Danel Ahman, Robert Atkey, Guido Mart\u00ednez, Catalin Hritcu, Exequiel Rivas, and \u00c9ric Tanter. 2019. Dijkstra monads for all. PACMPL 3, ICFP (2019), 104:1\u2013104:29. https:\/\/doi.org\/10.1145\/3341708 10.1145\/3341708","journal-title":"PACMPL"},{"key":"e_1_3_2_28_2","first-page":"87:1","article-title":"A verified messaging system","volume":"1","author":"Mansky William","year":"2017","unstructured":"William Mansky, Andrew W. Appel, and Aleksey Nogin. 2017. A verified messaging system. PACMPL 1, OOPSLA (2017), 87:1\u201387:28. https:\/\/doi.org\/10.1145\/3133911 10.1145\/3133911","journal-title":"PACMPL"},{"key":"e_1_3_2_29_2","first-page":"148","article-title":"An Iris Instance for Verifying CompCert C Programs","volume":"8","author":"Mansky William","year":"2024","unstructured":"William Mansky and Ke Du. 2024. An Iris Instance for Verifying CompCert C Programs. PACMPL 8, POPL (2024), 148\u2013174. https:\/\/doi.org\/10.1145\/3632848 10.1145\/3632848","journal-title":"PACMPL"},{"key":"e_1_3_2_30_2","first-page":"1378","article-title":"A concurrent program logic with a future and history","volume":"6","author":"Meyer Roland","year":"2022","unstructured":"Roland Meyer, Thomas Wies, and Sebastian Wolff. 2022. A concurrent program logic with a future and history. PACMPL 6, OOPSLA2 (2022), 1378\u20131407. https:\/\/doi.org\/10.1145\/3563337 10.1145\/3563337","journal-title":"PACMPL"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_3_2_32_2","first-page":"256","volume-title":"LNCS","author":"Rewitzky Ingrid","year":"2003","unstructured":"Ingrid Rewitzky. 2003. Binary Multirelations. In Theory and Applications of Relational Structures as Knowledge Instruments. LNCS, Vol. 2929.Springer, 256\u2013271. https:\/\/doi.org\/10.1007\/978-3-540-24615-2_12 10.1007\/978-3-540-24615-2_12"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523434"},{"key":"e_1_3_2_34_2","first-page":"158","article-title":"RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types","author":"Sammler Michael","year":"2021","unstructured":"Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, and Deepak Garg. 2021. RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types. In PLDI. 158\u2013174. https:\/\/doi.org\/10.1145\/3453483.3454036 10.1145\/3453483.3454036","journal-title":"PLDI"},{"key":"e_1_3_2_35_2","first-page":"775","article-title":"DimSum: A Decentralized Approach to Multi-language Semantics and Verification","volume":"7","author":"Sammler Michael","year":"2023","unstructured":"Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg, and Derek Dreyer. 2023. DimSum: A Decentralized Approach to Multi-language Semantics and Verification. PACMPL 7, POPL (2023), 775\u2013805. https:\/\/doi.org\/10.1145\/3571220 10.1145\/3571220","journal-title":"PACMPL"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3600006.3613172"},{"key":"e_1_3_2_37_2","first-page":"1","article-title":"Dijkstra monads forever: termination-sensitive specifications for interaction trees","volume":"5","author":"Silver Lucas","year":"2021","unstructured":"Lucas Silver and Steve Zdancewic. 2021. Dijkstra monads forever: termination-sensitive specifications for interaction trees. PACMPL 5, POPL (2021), 1\u201328. https:\/\/doi.org\/10.1145\/3434307 10.1145\/3434307","journal-title":"PACMPL"},{"key":"e_1_3_2_38_2","first-page":"1121","article-title":"Conditional Contextual Refinement","volume":"7","author":"Song Youngju","year":"2023","unstructured":"Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, and Derek Dreyer. 2023. Conditional Contextual Refinement. PACMPL 7, POPL (2023), 1121\u20131151. https:\/\/doi.org\/10.1145\/3571232 10.1145\/3571232","journal-title":"PACMPL"},{"key":"e_1_3_2_39_2","first-page":"283","article-title":"Later credits: resourceful reasoning for the later modality","volume":"6","author":"Spies Simon","year":"2022","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","journal-title":"PACMPL"},{"key":"e_1_3_2_40_2","doi-asserted-by":"crossref","unstructured":"Kasper Svendsen and Lars Birkedal. 2014. Impredicative Concurrent Abstract Predicates. In ESOP (LNCS Vol. 8410). 149\u2013168. 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_2_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39038-8_14"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491978"},{"key":"e_1_3_2_43_2","unstructured":"The Coq Team. 2024.The Coq proof assistant. https:\/\/coq.inria.fr\/."},{"key":"e_1_3_2_44_2","unstructured":"The Coq Team. 2024.The Logic of Coq. https:\/\/github.com\/coq\/coq\/wiki\/The-Logic-of-Coq. Accessed: 2024-10-18."},{"key":"e_1_3_2_45_2","unstructured":"The Iris Team. 2024.The Iris 4.2 Reference. https:\/\/plv.mpi-sws.org\/iris\/appendix-4.2.pdf"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660243"},{"key":"e_1_3_2_47_2","unstructured":"Max Vistrup Michael Sammler and Ralf Jung. 2024. Artifact of\u201cProgram logics \u00e0 la carte\u201d. https:\/\/doi.org\/10.5281\/zenodo.14180355 10.5281\/zenodo.14180355 Development version: https:\/\/gitlab.mpi-sws.org\/iris\/itree-program-logic."},{"key":"e_1_3_2_48_2","unstructured":"Vladimir Voevodsky. 2024. Forum discussion on \u2018coinductives\u2019. https:\/\/groups.google.com\/g\/homotopytypetheory\/c\/tYRTcI2Opyo\/m\/PIrI6t5me-oJ. Accessed: 2024-24."},{"key":"e_1_3_2_49_2","first-page":"51:1","article-title":"Interaction trees: representing recursive and impure programs in Coq","volume":"4","author":"Xia Li-yao","year":"2020","unstructured":"Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. 2020. Interaction trees: representing recursive and impure programs in Coq. PACMPL 4, POPL (2020), 51:1\u201351:32. https:\/\/doi.org\/10.1145\/3371119 10.1145\/3371119","journal-title":"PACMPL"},{"key":"e_1_3_2_50_2","first-page":"1","article-title":"Modular, compositional, and executable formal semantics for LLVM IR","volume":"5","author":"Zakowski Yannick","year":"2021","unstructured":"Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva, and Steve Zdancewic. 2021. Modular, compositional, and executable formal semantics for LLVM IR. PACMPL 5, ICFP (2021), 1\u201330. https:\/\/doi.org\/10.1145\/3473572 10.1145\/3473572","journal-title":"PACMPL"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/3586045"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704847","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704847","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:15:11Z","timestamp":1770200111000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704847"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":50,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704847"],"URL":"https:\/\/doi.org\/10.1145\/3704847","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}