{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,26]],"date-time":"2026-09-26T08:58:33Z","timestamp":1790413113663,"version":"4.1.0"},"reference-count":73,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2026,8,17]],"date-time":"2026-08-17T00:00:00Z","timestamp":1786924800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"National Science Foundation","award":["2338317"],"award-info":[{"award-number":["2338317"]}]},{"name":"National Science Foundation","award":["2319168"],"award-info":[{"award-number":["2319168"]}]},{"name":"Carlsberg Foundation","award":["CF23-0791"],"award-info":[{"award-number":["CF23-0791"]}],"id":[{"id":"https:\/\/ror.org\/01kpjmx04","id-type":"ROR","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,8,17]]},"abstract":"<jats:p>\n                    Traditionally, proof systems such as program logics come with two core theorems:\n                    <jats:italic toggle=\"yes\">soundness<\/jats:italic>\n                    and\n                    <jats:italic toggle=\"yes\">completeness<\/jats:italic>\n                    . The role of soundness is obvious: we want to be sure that arguments carried out inside the logic actually lead to correct conclusions. Completeness complements that by ensuring that the logic does not limit expressivity: in principle, any correct result can be obtained within the confines of the logic. This result typically has to be stated\n                    <jats:italic toggle=\"yes\">relative<\/jats:italic>\n                    to the completeness of the assertion logic that is used to reason about pre- and postconditions.\n                  <\/jats:p>\n                  <jats:p>Over the past decade, the Iris framework has emerged as a widely used foundation for building separation logics. While Iris-based logics typically come with a soundness proof, none of them have a proof of completeness. In this paper, we present the first approach for establishing completeness of Iris-based program logics, and we show the generality of our methodology by applying it to a range of different logics described in prior work, including partial and total concurrent separation logics for a higher-order ML-like language, two quantitative logics (for bounding execution time and probabilistic errors), and a relational logic for proving refinement. All our results have been mechanized in Rocq.<\/jats:p>","DOI":"10.1145\/3828682","type":"journal-article","created":{"date-parts":[[2026,8,17]],"date-time":"2026-08-17T20:23:46Z","timestamp":1786998226000},"page":"267-302","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Completeness of Iris-Based Program Logics"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5038-8283","authenticated-orcid":false,"given":"Johannes","family":"Hostert","sequence":"first","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-1151-6149","authenticated-orcid":false,"given":"Zichen","family":"Zhang","sequence":"additional","affiliation":[{"name":"New York University, New York, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-7095-564X","authenticated-orcid":false,"given":"Puming","family":"Liu","sequence":"additional","affiliation":[{"name":"NYU Shanghai, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6045-5232","authenticated-orcid":false,"given":"Simon Oddershede","family":"Gregersen","sequence":"additional","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7669-6348","authenticated-orcid":false,"given":"Ralf","family":"Jung","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5692-3347","authenticated-orcid":false,"given":"Joseph","family":"Tassarotti","sequence":"additional","affiliation":[{"name":"New York University, New York, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,8,17]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674635"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3776701"},{"key":"e_1_3_1_4_1","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. 109\u2013122. doi:10.1145\/1190216.1190235","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_6"},{"key":"e_1_3_1_6_1","unstructured":"Lars Birkedal and Ale\u0161 Bizjak. 2023. Lecture Notes on Iris: Higher-Order Concurrent Separation Logic. https:\/\/iris-project.org\/tutorial-material.html. https:\/\/iris-project.org\/tutorial-pdfs\/iris-lecture-notes.pdf Aarhus University."},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(4:1)2012"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_4"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","unstructured":"Tej Chajed Joseph Tassarotti M. Frans Kaashoek and Nickolai Zeldovich. 2019. Verifying concurrent crash-safe systems with Perennial. In Proceedings of the 27th ACM Symposium on Operating Systems Principles SOSP 2019 Huntsville ON Canada October 27-30 2019. 243\u2013258. doi:10.1145\/3341301.3359632","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_3_1_10_1","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 OSDI. 423\u2013439. https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/chajed"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034574.2034828"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.15352\/bjma\/1240321550"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1137\/0207005"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371102"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-97439-7_15"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","unstructured":"Paulo Em\u00edlio de Vilhena and Fran\u00e7ois Pottier. 2023. A Type System for Effect Handlers and Dynamic Labels. In ESOP. 225\u2013252. doi:10.1007\/978-3-031-30044-8_9","DOI":"10.1007\/978-3-031-30044-8_9"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656422"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498689"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704859"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408996"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","unstructured":"Simon Oddershede Gregersen Chaitanya Agarwal and Joseph Tassarotti. 2025. Logical Relations for Formally Verified Authenticated Data Structures. In Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security CCS 2025 Taipei Taiwan October 13-17 2025. 1394\u20131408. doi:10.1145\/3719027.3744801","DOI":"10.1145\/3719027.3744801"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674632"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632868"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434291"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622823"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704877"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689753"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_9"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371074"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/355620.361161"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.5"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","unstructured":"Johannes Hostert Zichen Zhang Puming Liu Simon Oddershede Gregersen Ralf Jung and Joseph Tassarotti. 2026. Completeness of Iris-Based Program Logics (Artifact). doi:10.5281\/zenodo.20625901","DOI":"10.5281\/zenodo.20625901"},{"key":"e_1_3_1_33_1","unstructured":"Iris developers and contributors. 2026. The Iris 4.5 Reference. https:\/\/plv.mpi-sws.org\/iris\/appendix-4.5.pdf"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","unstructured":"Samin S. Ishtiaq and Peter W. O\u2019Hearn. 2001. BI as an Assertion Language for Mutable Data Structures. In POPL. 14\u201326. doi:10.1145\/360204.375719","DOI":"10.1145\/360204.375719"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","unstructured":"Jan-Oliver Kaiser Hoang-Hai Dang Derek Dreyer Ori Lahav and Viktor Vafeiadis. 2017. Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. In 31st European Conference on Object-Oriented Programming ECOOP 2017 Barcelona Spain June 19-23 2017. 17:1\u201317:29. doi:10.4230\/LIPIcs.ECOOP.2017.17","DOI":"10.4230\/LIPIcs.ECOOP.2017.17"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_3_1_43_1","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. doi:10.1145\/3009837.3009855","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2025.27"},{"key":"e_1_3_1_45_1","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. 336\u2013365. doi:10.1007\/978-3-030-44914-8_13","DOI":"10.1007\/978-3-030-44914-8_13"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1093\/COMJNL\/6.4.308"},{"key":"e_1_3_1_47_1","unstructured":"Xavier Leroy Andrew Appel Sandrine Blazy and Gordon Stewart. 2012. The CompCert memory model version 2. Technical Report RR-7987. Inria. https:\/\/hal.inria.fr\/hal-00703441"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3747514"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.2307\/2266895"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704899"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632848"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","unstructured":"Yusuke Matsushita Xavier Denis Jacques-Henri Jourdan and Derek Dreyer. 2022. RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code. In PLDI. 841\u2013856. doi:10.1145\/3519939.3523704","DOI":"10.1145\/3519939.3523704"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158121"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473571"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_1"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3776655"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571218"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","unstructured":"Hiroshi Nakano. 2000. A Modality for Recursion. In 15th Annual IEEE Symposium on Logic in Computer Science Santa Barbara California USA June 26-29 2000. 255\u2013266. doi:10.1109\/LICS.2000.855774","DOI":"10.1109\/LICS.2000.855774"},{"key":"e_1_3_1_59_1","unstructured":"Susan S. Owicki. 1975. Axiomatic Proof Techniques for Parallel Programs. Ph. D. Dissertation. Cornell University."},{"key":"e_1_3_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_3_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632892"},{"key":"e_1_3_1_62_1","doi-asserted-by":"publisher","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. doi:10.1145\/3453483.3454036","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_3_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3747509"},{"key":"e_1_3_1_64_1","doi-asserted-by":"publisher","unstructured":"Upamanyu Sharma Ralf Jung Joseph Tassarotti M. Frans Kaashoek and Nickolai Zeldovich. 2023. Grove: a Separation-Logic Library for Verifying Distributed Systems. In SOSP. 113\u2013129. doi:10.1145\/3600006.3613172","DOI":"10.1145\/3600006.3613172"},{"key":"e_1_3_1_65_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90033-3"},{"key":"e_1_3_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_3_1_67_1","unstructured":"The Rocq Team. 2026. The Rocq Prover. https:\/\/rocq-prover.org\/."},{"key":"e_1_3_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632851"},{"key":"e_1_3_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3676954"},{"key":"e_1_3_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_3_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704841"},{"key":"e_1_3_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211617"},{"key":"e_1_3_1_73_1","unstructured":"Hongseok Yang. 2001. Local reasoning for stateful programs. Ph. D. Dissertation. USA. Advisor(s) Reddy Uday S. AAI3023240."},{"key":"e_1_3_1_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45931-6_28"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3828682","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3828682","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,9,26]],"date-time":"2026-09-26T08:11:56Z","timestamp":1790410316000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3828682"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,8,17]]},"references-count":73,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2026,8,17]]}},"alternative-id":["10.1145\/3828682"],"URL":"https:\/\/doi.org\/10.1145\/3828682","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,8,17]]},"assertion":[{"value":"2026-02-19","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-05-13","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-08-17","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}