{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,6]],"date-time":"2026-06-06T03:48:29Z","timestamp":1780717709049,"version":"3.54.1"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2020,8,2]],"date-time":"2020-08-02T00:00:00Z","timestamp":1596326400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100007601","name":"Horizon 2020 Framework Programme","doi-asserted-by":"publisher","award":["834146"],"award-info":[{"award-number":["834146"]}],"id":[{"id":"10.13039\/501100007601","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100011199","name":"European Research Council","doi-asserted-by":"publisher","award":["683032"],"award-info":[{"award-number":["683032"]}],"id":[{"id":"10.13039\/100011199","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100015089","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-18-1-2892"],"award-info":[{"award-number":["N00014-18-1-2892"]}],"id":[{"id":"10.13039\/100015089","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":[[2020,8,2]]},"abstract":"<jats:p>Much recent research has been devoted to modeling effects within type theory. Building on this work, we observe that effectful type theories can provide a foundation on which to build semantics for more complex programming constructs and program logics, extending the reasoning principles that apply within the host effectful type theory itself.<\/jats:p>\n          <jats:p>\n            Concretely, our main contribution is a semantics for concurrent separation logic (CSL) within the F\n            <jats:sup>\u22c6<\/jats:sup>\n            proof assistant in a manner that enables dependently typed, effectful F\n            <jats:sup>\u22c6<\/jats:sup>\n            programs to make use of concurrency and to be specified and verified using a full-featured, extensible CSL. In contrast to prior approaches, we directly derive the partial-correctness Hoare rules for CSL from the denotation of computations in the\n            <jats:italic>effectful<\/jats:italic>\n            semantics of non-deterministically interleaved atomic actions.\n          <\/jats:p>\n          <jats:p>Demonstrating the flexibility of our semantics, we build generic, verified libraries that support various concurrency constructs, ranging from dynamically allocated, storable spin locks, to protocol-indexed channels. We conclude that our effectful semantics provides a simple yet expressive basis on which to layer domain-specific languages and logics for verified, concurrent programming.<\/jats:p>","DOI":"10.1145\/3409003","type":"journal-article","created":{"date-parts":[[2020,8,3]],"date-time":"2020-08-03T13:48:02Z","timestamp":1596462482000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":25,"title":["SteelCore: an extensible concurrent separation logic for effectful dependently typed programs"],"prefix":"10.1145","volume":"4","author":[{"given":"Nikhil","family":"Swamy","sequence":"first","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aseem","family":"Rastogi","sequence":"additional","affiliation":[{"name":"Microsoft Research, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aymeric","family":"Fromherz","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Denis","family":"Merigoux","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Danel","family":"Ahman","sequence":"additional","affiliation":[{"name":"University of Ljubljana, Slovenia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Guido","family":"Mart\u00ednez","sequence":"additional","affiliation":[{"name":"CIFASIS-CONICET, Argentina"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2020,8,3]]},"reference":[{"key":"e_1_2_2_1_1","first-page":"65","article-title":"Recalling a witness: Foundations and applications of monotonic state","volume":"2","author":"Ahman D.","year":"2018","journal-title":"PACMPL"},{"key":"e_1_2_2_2_1","volume-title":"Parameterised notions of computation. Journal of Functional Programming, 19 : 335-376","author":"Atkey R.","year":"2009"},{"key":"e_1_2_2_3_1","first-page":"25","article-title":"Interleaving data and efects","author":"Atkey R.","year":"2015","journal-title":"Journal of Functional Programming"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158104"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_4"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500581"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_2"},{"key":"e_1_2_2_8_1","volume-title":"Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVII).","author":"Buisse A."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_2_2_11_1","volume-title":"Verifying custom synchronization constructs using higher-order separation logic. ACM Trans. Program. Lang. Syst., 38 ( 2 )","author":"Dodds M.","year":"2016"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291168"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462160"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76637-7_3"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44622-2_21"},{"key":"e_1_2_2_16_1","volume-title":"Proc. ACM Program. Lang., 4(POPL)","author":"Hinrichsen J. K.","year":"2019"},{"key":"e_1_2_2_17_1","first-page":"2008","article-title":"Oracle semantics for concurrent separation logic. In S. Drossopoulou, editor, Programming Languages and Systems, 17th European Symposium on Programming, ESOP 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest","author":"Hobor A.","year":"2008","journal-title":"Hungary, March 29-"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053567"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_19"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_2_21_1","volume-title":"Proc. ACM Program. Lang., 2(POPL)","author":"Jung R.","year":"2017"},{"key":"e_1_2_2_22_1","volume-title":"Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program., 28 : e20","author":"Jung R.","year":"2018"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804319"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_2_25_1","volume-title":"Aneris: A mechanised logic for modular reasoning about distributed systems. Submitted for publication","author":"Krogh-Jespersen M.","year":"2019"},{"key":"e_1_2_2_26_1","volume-title":"Meta-F* : Proof automation with SMT, tactics, and metaprograms. ESOP","author":"Mart\u00ednez G.","year":"2019"},{"key":"e_1_2_2_27_1","volume-title":"Kleisli arrows of outrageous fortune","author":"McBride C.","year":"2011"},{"key":"e_1_2_2_28_1","volume-title":"Hoare type theory, polymorphism and separation. JFP, 18 ( 5-6 ): 865-911","author":"Nanevski A.","year":"2008"},{"key":"e_1_2_2_29_1","volume-title":"Structuring the verification of heap-manipulating programs. POPL","author":"Nanevski A.","year":"2010"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_16"},{"key":"e_1_2_2_31_1","first-page":"161","article-title":"Specifying concurrent programs in separation logic: morphisms and simulations","volume":"3","author":"Nanevski A.","year":"2019","journal-title":"PACMPL"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_4"},{"key":"e_1_2_2_33_1","volume-title":"The relationship between separation logic and implicit dynamic frames. Logical Methods in Computer Science, 8 ( 3 :01): 1-54","author":"Parkinson M. J.","year":"2012"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209166"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373818"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737964"},{"key":"e_1_2_2_38_1","volume-title":"Implicit dynamic frames. ACM Trans. Program. Lang. Syst., 34 ( 1 )","author":"Smans J.","year":"2012"},{"key":"e_1_2_2_39_1","volume-title":"Secure distributed programming with value-dependent types. ICFP","author":"Swamy N.","year":"2011"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034778"},{"key":"e_1_2_2_41_1","volume-title":"Dependent types and multi-monadic efects in F*. POPL","author":"Swamy N.","year":"2016"},{"key":"e_1_2_2_42_1","volume-title":"Data types \u00e0 la carte. Journal of Functional Programming, 18 ( 4 ): 423-436","author":"Swierstra W.","year":"2008"},{"key":"e_1_2_2_43_1","first-page":"64","article-title":"A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runst","volume":"2","author":"Timany A.","year":"2018","journal-title":"PACMPL"},{"key":"e_1_2_2_44_1","volume-title":"Proc. ACM Program. Lang., 4(POPL)","author":"Xia L.-y.","year":"2019"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3409003","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3409003","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3409003","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:59Z","timestamp":1750193279000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3409003"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,8,2]]},"references-count":44,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2020,8,2]]}},"alternative-id":["10.1145\/3409003"],"URL":"https:\/\/doi.org\/10.1145\/3409003","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,8,2]]},"assertion":[{"value":"2020-08-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}