{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T18:11:54Z","timestamp":1775671914284,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":55,"publisher":"ACM","funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101171349"],"award-info":[{"award-number":["101171349"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Dutch Research Council (NWO)","award":["https:\/\/doi.org\/10.61686\/FHYZO53064"],"award-info":[{"award-number":["https:\/\/doi.org\/10.61686\/FHYZO53064"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2026,1,8]]},"DOI":"10.1145\/3779031.3779095","type":"proceedings-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:55:47Z","timestamp":1767898547000},"page":"248-263","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Building Blocks for Step-Indexed Program Logics"],"prefix":"10.1145","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-0001-6143-9031","authenticated-orcid":false,"given":"Jonas Kastberg","family":"Hinrichsen","sequence":"additional","affiliation":[{"name":"Aalborg University, Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2917-375X","authenticated-orcid":false,"given":"Lennard","family":"G\u00e4her","sequence":"additional","affiliation":[{"name":"MPI-SWS, Saarland Informatics Campus, Germany"}],"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":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Semantics of Types for Mutable State. Ph. D. Dissertation","author":"Ahmed Amal","unstructured":"Amal Ahmed. 2004. Semantics of Types for Mutable State. Ph. D. Dissertation. Princeton University."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Andrew W. Appel (Ed.). 2014. Program Logics for Certified Compilers. Cambridge University Press.","DOI":"10.1017\/CBO9781107256552"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_2_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. https:\/\/doi.org\/10.1145\/1190216.1190235 10.1145\/1190216.1190235","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2006.12.034"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-018-9457-5"},{"key":"e_1_3_2_1_7_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 SOSP. 243\u2013258. https:\/\/doi.org\/10.1145\/3341301.3359632 10.1145\/3341301.3359632","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_26"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434314"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3776676"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","unstructured":"Thomas Dinsdale-Young Lars Birkedal Philippa Gardner Matthew J. Parkinson and Hongseok Yang. 2013. Views: compositional reasoning for concurrent programs. 287\u2013300. https:\/\/doi.org\/10.1145\/2429069.2429104 10.1145\/2429069.2429104","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3729311"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473590"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","unstructured":"Dan Frumin Robbert Krebbers and Lars Birkedal. 2021. Compositional Non-Interference for Fine-Grained Concurrent Programs. In S&P. 1416\u20131433. https:\/\/doi.org\/10.1109\/SP40001.2021.00003 10.1109\/SP40001.2021.00003","DOI":"10.1109\/SP40001.2021.00003"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656422"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607859"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434291"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371074"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-18(2:16)2022"},{"key":"e_1_3_2_1_20_1","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_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78739-6_27"},{"key":"e_1_3_2_1_22_1","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_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_3_2_1_28_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. https:\/\/doi.org\/10.1145\/3009837.3009855 10.1145\/3009837.3009855","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_13"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3720525"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632848"},{"key":"e_1_3_2_1_32_1","volume-title":"Non-Step-Indexed Separation Logic with Invariants and Rust-Style Borrows. Ph. D. Dissertation","author":"Matsushita Yusuke","unstructured":"Yusuke Matsushita. 2023. Non-Step-Indexed Separation Logic with Invariants and Rust-Style Borrows. Ph. D. Dissertation. University of Tokyo."},{"key":"e_1_3_2_1_33_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. https:\/\/doi.org\/10.1145\/3519939.3523704 10.1145\/3519939.3523704","DOI":"10.1145\/3519939.3523704"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3729250"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_1"},{"key":"e_1_3_2_1_36_1","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_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2006.12.035"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_1_40_1","unstructured":"Upamanyu Sharma and Tej Chajed. 2025. Personal communication at 2025-08-25."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.17809073"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689732"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454031"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547631"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_28"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409003"},{"key":"e_1_3_2_1_49_1","unstructured":"The Iris Team. 2025. Global resource algebra management. https:\/\/gitlab.mpi-sws.org\/iris\/iris\/-\/blob\/master\/docs\/resource_algebras.md"},{"key":"e_1_3_2_1_50_1","unstructured":"The Iris Team. 2025. View Camera. https:\/\/gitlab.mpi-sws.org\/iris\/iris\/-\/blob\/master\/iris\/algebra\/view.v"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341709"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632851"},{"key":"e_1_3_2_1_53_1","unstructured":"Amin Timany and Jonas Kastberg Hinrichsen. 2022. Iris Gitlab merge request: Strengthened soundness theorem. https:\/\/gitlab.mpi-sws.org\/iris\/iris\/-\/merge_requests\/857"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3676954"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704841"}],"event":{"name":"CPP '26: 15th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Rennes France","acronym":"CPP '26","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3779031.3779095","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T16:54:12Z","timestamp":1775667252000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3779031.3779095"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":55,"alternative-id":["10.1145\/3779031.3779095","10.1145\/3779031"],"URL":"https:\/\/doi.org\/10.1145\/3779031.3779095","relation":{},"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}