{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T10:09:01Z","timestamp":1781258941772,"version":"3.54.1"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>PulseCore is a new program logic suitable for intrinsic proofs of higher-order, stateful, concurrent, dependently typed programs. It provides many of the features of a modern, concurrent separation logic, including dynamically allocated impredicative invariants, higher-order ghost state, step-indexing with later credits, and support for user-defined ghost state constructions. PulseCore is developed foundationally within the F\u2605 programming language with fully mechanized proofs, and is applicable to F\u2605 programs itself.<\/jats:p>\n          <jats:p>To evaluate our work, we use Pulse, a surface language within F\u2605 for PulseCore, to develop a range of program proofs. Illustrating its suitability for proving higher-order concurrent programs, we present a verified library for task pools in the style of OCaml5, together with some verified task-parallel programs. Next, we present various data structures and synchronization primitives, including a barrier that requires the use of higher-order ghost state. Finally, we present a verified implementation of the DICE Protection Environment, an industry standard secure boot protocol. Taken together, our evaluation consists of more than 31,000 lines of verified code in a range of settings, providing evidence that PulseCore is both highly expressive as well as practical for a variety of program proof applications.<\/jats:p>","DOI":"10.1145\/3729311","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"1516-1539","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4057-9574","authenticated-orcid":false,"given":"Gabriel","family":"Ebner","sequence":"first","affiliation":[{"name":"Microsoft Research, Redmond, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-5831-9991","authenticated-orcid":false,"given":"Guido","family":"Mart\u00ednez","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3283-8011","authenticated-orcid":false,"given":"Aseem","family":"Rastogi","sequence":"additional","affiliation":[{"name":"Microsoft Research, Bengaluru, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2719-4856","authenticated-orcid":false,"given":"Thibault","family":"Dardinier","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2245-2687","authenticated-orcid":false,"given":"Megan","family":"Frisella","sequence":"additional","affiliation":[{"name":"University of Washington, Seattle, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4590-9712","authenticated-orcid":false,"given":"Tahina","family":"Ramananandro","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9254-3015","authenticated-orcid":false,"given":"Nikhil","family":"Swamy","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292555"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158153"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_2"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575687"},{"key":"e_1_2_2_6_1","volume-title":"Everest: Towards a Verified, Drop-in Replacement of HTTPS. In 2nd Summit on Advances in Programming Languages","author":"Bhargavan Karthikeyan","year":"2017","unstructured":"Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, C\u00e9dric Fournet, Chris Hawblitzel, C\u0103t\u0103lin Hri\u0163cu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jianyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-B\u00e9guelin, and Jean-Karim Zinzindohou\u00e9. 2017. Everest: Towards a Verified, Drop-in Replacement of HTTPS. In 2nd Summit on Advances in Programming Languages. http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2017\/7119\/pdf\/LIPIcs-SNAPL-2017-1.pdf"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926401"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034828"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","unstructured":"Gabriel Ebner Guido Mart\u00ednez Aseem Rastogi Thibault Dardinier Megan Frisella Tahina Ramananandro and Nikhil Swamy. 2025. PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs\u2014PLDI 2025 Artifact. https:\/\/doi.org\/10.5281\/zenodo.15047546 10.5281\/zenodo.15047546","DOI":"10.5281\/zenodo.15047546"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632854"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656439"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706322"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926417"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_19"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371072"},{"key":"e_1_2_2_18_1","unstructured":"William Mansky. 2022. Bringing Iris into the Verified Software Toolchain. arxiv:2207.06574. arxiv:2207.06574"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632848"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408978"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360587"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_16"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"e_1_2_2_24_1","volume-title":"Concurrency and Local Reasoning. In CONCUR 2004 - Concurrency Theory, Philippa Gardner and Nobuko Yoshida (Eds.). Springer Berlin Heidelberg","author":"O\u2019Hearn Peter W.","year":"2004","unstructured":"Peter W. O\u2019Hearn. 2004. Resources, Concurrency and Local Reasoning. In CONCUR 2004 - Concurrency Theory, Philippa Gardner and Nobuko Yoshida (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 49\u201367. isbn:978-3-540-28644-8"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00114"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110261"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_25"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454031"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547631"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409003"},{"key":"e_1_2_2_34_1","volume-title":"30th USENIX Security Symposium (USENIX Security 21)","author":"Tao Zhe","unstructured":"Zhe Tao, Aseem Rastogi, Naman Gupta, Kapil Vaswani, and Aditya V. Thakur. 2021. DICE*: A Formally Verified Implementation of DICE Measured Boot. In 30th USENIX Security Symposium (USENIX Security 21). USENIX Association, 1091\u20131107. isbn:978-1-939133-24-3 https:\/\/www.usenix.org\/conference\/usenixsecurity21\/presentation\/tao"},{"key":"e_1_2_2_35_1","unstructured":"Trusted Computing Group. [n. d.]. DICE. https:\/\/trustedcomputinggroup.org\/work-groups\/dice-architectures\/"},{"key":"e_1_2_2_36_1","unstructured":"Trusted Computing Group. 2023. DICE Protection Environment. https:\/\/trustedcomputinggroup.org\/wp-content\/uploads\/TCG-DICE-Protection-Environment-Specification_14february2023-1.pdf"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729311","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T06:08:40Z","timestamp":1752646120000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729311"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":37,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729311"],"URL":"https:\/\/doi.org\/10.1145\/3729311","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}