{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:50Z","timestamp":1780994750083,"version":"3.54.1"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T00:00:00Z","timestamp":1629331200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000879","name":"Alfred P. Sloan Foundation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000879","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100002418","name":"Intel Corporation","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100002418","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["DGE174501"],"award-info":[{"award-number":["DGE174501"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-18-1-289"],"award-info":[{"award-number":["N00014-18-1-289"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["CIRCUS 683032"],"award-info":[{"award-number":["CIRCUS 683032"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,8,22]]},"abstract":"<jats:p>\n            Steel is a language for developing and proving concurrent programs embedded in F\n            <jats:sup>\u22c6<\/jats:sup>\n            , a dependently typed programming language and proof assistant. Based on SteelCore, a concurrent separation logic (CSL) formalized in F\n            <jats:sup>\u22c6<\/jats:sup>\n            , our work focuses on exposing the proof rules of the logic in a form that enables programs and proofs to be effectively co-developed.\n          <\/jats:p>\n          <jats:p>\n            Our main contributions include a new formulation of a Hoare logic of\n            <jats:italic>quintuples<\/jats:italic>\n            involving both separation logic and first-order logic, enabling efficient verification condition (VC) generation and proof discharge using a combination of tactics and SMT solving. We relate the VCs produced by our quintuple system to solving a system of associativity-commutativity (AC) unification constraints and develop tactics to (partially) solve these constraints using AC-matching modulo SMT-dischargeable equations.\n          <\/jats:p>\n          <jats:p>\n            Our system is fully mechanized and implemented in F\n            <jats:sup>\u22c6<\/jats:sup>\n            . We evaluate it by developing several verified programs and libraries, including various sequential and concurrent linked data structures, proof libraries, and a library for 2-party session types. Our experience leads us to conclude that our system enables a mixture of automated and interactive proof, making it productive to build programs foundationally verified against a highly expressive, state-of-the-art CSL.\n          <\/jats:p>","DOI":"10.1145\/3473590","type":"journal-article","created":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T10:44:29Z","timestamp":1629369869000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["Steel: proof-oriented programming in a dependently typed concurrent separation logic"],"prefix":"10.1145","volume":"5","author":[{"given":"Aymeric","family":"Fromherz","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aseem","family":"Rastogi","sequence":"additional","affiliation":[{"name":"Microsoft Research, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nikhil","family":"Swamy","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sydney","family":"Gibson","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Guido","family":"Mart\u00ednez","sequence":"additional","affiliation":[{"name":"CIFASIS-CONICET, Argentina"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2247-0938","authenticated-orcid":false,"given":"Denis","family":"Merigoux","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tahina","family":"Ramananandro","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,8,19]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/1987211.1987212"},{"key":"e_1_2_2_2_1","volume-title":"O\u2019hearn","author":"Berdine Josh","year":"2005"},{"key":"e_1_2_2_3_1","unstructured":"Edwin Brady. 2016. Type-driven Development With Idris. Manning. isbn:9781617293023 http:\/\/www.worldcat.org\/isbn\/9781617293023  Edwin Brady. 2016. Type-driven Development With Idris. Manning. isbn:9781617293023 http:\/\/www.worldcat.org\/isbn\/9781617293023"},{"key":"e_1_2_2_4_1","volume-title":"Petersen","author":"Brotherston James","year":"2012"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034828"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993526"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110278"},{"key":"e_1_2_2_9_1","volume-title":"Associative-Commutative Unification. In 7th International Conference on Automated Deduction, R. E. Shostak (Ed.). Springer New York","author":"Fages Fran\u00e7ois","year":"1984"},{"key":"e_1_2_2_10_1","unstructured":"Georges Gonthier Assia Mahboubi and Enrico Tassi. 2016. A Small Scale Reflection Extension for the Coq system. Inria Saclay Ile de France. https:\/\/hal.inria.fr\/inria-00258384  Georges Gonthier Assia Mahboubi and Enrico Tassi. 2016. A Small Scale Reflection Extension for the Coq system. Inria Saclay Ile de France. https:\/\/hal.inria.fr\/inria-00258384"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371074"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429131"},{"key":"e_1_2_2_13_1","volume-title":"Automated Technology for Verification and Analysis, Franck Cassez and Jean-Fran\u00e7ois Raskin (Eds.)","author":"Iosif Radu"},{"key":"e_1_2_2_14_1","volume-title":"Assertion Language for Mutable Data Structures. In Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Samin","year":"2001"},{"key":"e_1_2_2_15_1","doi-asserted-by":"crossref","unstructured":"Bart Jacobs Jan Smans Pieter Philippaerts Fr\u00e9d\u00e9ric Vogels Willem Penninckx and Frank Piessens. 2011. VeriFast: A Powerful Sound Predictable Fast Verifier for C and Java. In NASA Formal Methods.  Bart Jacobs Jan Smans Pieter Philippaerts Fr\u00e9d\u00e9ric Vogels Willem Penninckx and Frank Piessens. 2011. VeriFast: A Powerful Sound Predictable Fast Verifier for C and Java. In NASA Formal Methods.","DOI":"10.1007\/978-3-642-20398-5_4"},{"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\/36330.36332"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_2_2_19_1","volume-title":"Leino and Micha\u0142 Moskal","author":"K. Rustan","year":"2010"},{"key":"e_1_2_2_20_1","volume-title":"Gorrieri (Eds.) (Lecture Notes in Computer Science","volume":"222","author":"Leino K. R. M."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_2"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/248052.248106"},{"key":"e_1_2_2_23_1","volume-title":"Viper: A Verification Infrastructure for Permission-Based Reasoning. In Verification, Model Checking, and Abstract Interpretation (VMCAI)","author":"M\u00fcller P.","year":"2016"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360587"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_2_2_27_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"},{"key":"e_1_2_2_28_1","doi-asserted-by":"crossref","unstructured":"Susan Owicki and David Gries. 1976. Verifying Properties of Parallel Programs: An Axiomatic Approach. Commun. ACM.  Susan Owicki and David Gries. 1976. Verifying Properties of Parallel Programs: An Axiomatic Approach. Commun. ACM.","DOI":"10.1145\/360051.360224"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(3:1)2012"},{"key":"e_1_2_2_30_1","unstructured":"Aseem Rastogi Guido Mart\u00ednez Aymeric Fromherz Tahina Ramananandro and Nikhil Swamy. 2020. Layered Indexed Effects: Foundations and Applications of Effectful Dependently Typed Programming. https:\/\/www.fstar-lang.org\/papers\/layeredeffects\/ In submission.  Aseem Rastogi Guido Mart\u00ednez Aymeric Fromherz Tahina Ramananandro and Nikhil Swamy. 2020. Layered Indexed Effects: Foundations and Applications of Effectful Dependently Typed Programming. https:\/\/www.fstar-lang.org\/papers\/layeredeffects\/ In submission."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_2_2_32_1","doi-asserted-by":"crossref","unstructured":"M. Sammler R. Lepigre R. Krebbers K. Memarian D. Dreyer and D. Garg. 2021. RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types. In to appear in Programming Languages Design and Implementation (PLDI). ACM.  M. Sammler R. Lepigre R. Krebbers K. Memarian D. Dreyer and D. Garg. 2021. RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types. In to appear in Programming Languages Design and Implementation (PLDI). ACM.","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409003"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491978"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439930"},{"key":"e_1_2_2_37_1","unstructured":"Hongseok Yang Oukseh Lee Josh Berdine Cristiano Calcagno Byron Cook and Dino Distefano. 2008. Scalable shape analysis for systems code. In In CAV.  Hongseok Yang Oukseh Lee Josh Berdine Cristiano Calcagno Byron Cook and Dino Distefano. 2008. Scalable shape analysis for systems code. In In CAV."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473590","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3473590","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3473590","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:28:16Z","timestamp":1750195696000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473590"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,19]]},"references-count":37,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2021,8,22]]}},"alternative-id":["10.1145\/3473590"],"URL":"https:\/\/doi.org\/10.1145\/3473590","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,8,19]]},"assertion":[{"value":"2021-08-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}