{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:07:48Z","timestamp":1784200068072,"version":"3.55.0"},"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>\n                    <jats:sc>PulseCore<\/jats:sc>\n                    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.\n                    <jats:sc>PulseCore<\/jats:sc>\n                    is developed foundationally within the\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:msup>\n                          <mml:mrow>\n                            <mml:mi mathvariant=\"normal\">F<\/mml:mi>\n                          <\/mml:mrow>\n                          <mml:mrow>\n                            <mml:mo>\u22c6<\/mml:mo>\n                          <\/mml:mrow>\n                        <\/mml:msup>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    programming language with fully mechanized proofs, and is applicable to\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:msup>\n                          <mml:mrow>\n                            <mml:mi mathvariant=\"normal\">F<\/mml:mi>\n                          <\/mml:mrow>\n                          <mml:mrow>\n                            <mml:mo>\u22c6<\/mml:mo>\n                          <\/mml:mrow>\n                        <\/mml:msup>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    programs itself.\n                  <\/jats:p>\n                  <jats:p>\n                    To evaluate our work, we use\n                    <jats:sc>Pulse<\/jats:sc>\n                    , a surface language within\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:msup>\n                          <mml:mrow>\n                            <mml:mi mathvariant=\"normal\">F<\/mml:mi>\n                          <\/mml:mrow>\n                          <mml:mrow>\n                            <mml:mo>\u22c6<\/mml:mo>\n                          <\/mml:mrow>\n                        <\/mml:msup>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    for\n                    <jats:sc>PulseCore<\/jats:sc>\n                    , 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\n                    <jats:sc>PulseCore<\/jats:sc>\n                    is both highly expressive as well as practical for a variety of program proof applications.\n                  <\/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_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292555"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158153"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_2"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575687"},{"key":"e_1_3_2_7_1","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 ZanellaB\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_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926401"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034828"},{"key":"e_1_3_2_10_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-PLDI 2025 Artifact. doi:10.5281\/zenodo.15047546","DOI":"10.5281\/zenodo.15047546"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632854"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656439"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706322"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926417"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_19"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371072"},{"key":"e_1_3_2_19_1","unstructured":"William Mansky. 2022. Bringing Iris into the Verified Software Toolchain. arXiv:2207.06574 [cs.PL] https:\/\/arxiv.org\/abs\/2207.06574"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632848"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408978"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360587"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_16"},{"key":"e_1_3_2_24_1","doi-asserted-by":"crossref","unstructured":"Aleksandar Nanevski J.Gregory Morrisett and Lars Birkedal. 2008. Hoare type theory polymorphism and separation. J. Funct. Program. 18 5-6 (2008) 865\u2013911. http:\/\/ynot.cs.harvard.edu\/papers\/jfpsep07.pdf","DOI":"10.1017\/S0956796808006953"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_4"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","unstructured":"Jonathan Protzenko Bryan Parno Aymeric Fromherz Chris Hawblitzel Marina Polubelova Karthikeyan Bhargavan Benjamin Beurdouche Joonwon Choi Antoine Delignat-Lavaud C\u00e9dric Fournet Natalia Kulatova Tahina Ramananandro Aseem Rastogi Nikhil Swamy Christoph M. Wintersteiger and Santiago Zanella-Beguelin. 2020. EverCrypt: A Fast Verified Cross-Platform Cryptographic Provider. In 2020 IEEE Symposium on Security and Privacy (SP). 983\u2013983. doi:10.1109\/SP40000.2020.00114","DOI":"10.1109\/SP40000.2020.00114"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110261"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_25"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454031"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547631"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409003"},{"key":"e_1_3_2_35_1","first-page":"1091","volume-title":"30th USENIX Security Symposium (USENIX Security","author":"Tao Zhe","year":"2021","unstructured":"Zhe Tao, Aseem Rastogi, Naman Gupta, Kapil Vaswani, and AdityaV. Thakur. 2021. DICE*: A Formally Verified Implementation of DICE Measured Boot. In 30th USENIX Security Symposium (USENIX Security 21). USENIX Association, 1091\u20131091. https:\/\/www.usenix.org\/conference\/usenixsecurity21\/presentation\/tao"},{"key":"e_1_3_2_36_1","unstructured":"Trusted Computing Group. [n. d.]. DICE. https:\/\/trustedcomputinggroup.org\/work-groups\/dice-architectures\/."},{"key":"e_1_3_2_37_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_3_2_38_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":[[2026,7,16]],"date-time":"2026-07-16T10:09:23Z","timestamp":1784196563000},"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"}}]}}