{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:14:39Z","timestamp":1775873679723,"version":"3.50.1"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2018,7,30]],"date-time":"2018-07-30T00:00:00Z","timestamp":1532908800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001665","name":"French National Research Agency","doi-asserted-by":"crossref","award":["ANR-15-CE25-0008"],"award-info":[{"award-number":["ANR-15-CE25-0008"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"crossref"}]},{"name":"European Research Council","award":["683289"],"award-info":[{"award-number":["683289"]}]},{"name":"Flemish Research Fund","award":["G.0962.17N"],"award-info":[{"award-number":["G.0962.17N"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,7,30]]},"abstract":"<jats:p>A number of tools have been developed for carrying out separation-logic proofs mechanically using an interactive proof assistant. One of the most advanced such tools is the Iris Proof Mode (IPM) for Coq, which offers a rich set of tactics for making separation-logic proofs look and feel like ordinary Coq proofs. However, IPM is tied to a particular separation logic (namely, Iris), thus limiting its applicability.<\/jats:p><jats:p>In this paper, we propose MoSeL, a general and extensible Coq framework that brings the benefits of IPM to a much larger class of separation logics. Unlike IPM, MoSeL is applicable to both affine and linear separation logics (and combinations thereof), and provides generic tactics that can be easily extended to account for the bespoke connectives of the logics with which it is instantiated. To demonstrate the effectiveness of MoSeL, we have instantiated it to provide effective tactical support for interactive and semi-automated proofs in six very different separation logics.<\/jats:p>","DOI":"10.1145\/3236772","type":"journal-article","created":{"date-parts":[[2018,7,31]],"date-time":"2018-07-31T19:41:18Z","timestamp":1533066078000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":61,"title":["MoSeL: a general, extensible modal framework for interactive proofs in separation logic"],"prefix":"10.1145","volume":"2","author":[{"given":"Robbert","family":"Krebbers","sequence":"first","affiliation":[{"name":"Delft University of Technology, Netherlands"}]},{"given":"Jacques-Henri","family":"Jourdan","sequence":"additional","affiliation":[{"name":"LRI, France \/ University of Paris-Sud, France \/ CNRS, France \/ University of Paris-Saclay, France"}]},{"given":"Ralf","family":"Jung","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]},{"given":"Joseph","family":"Tassarotti","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}]},{"given":"Jan-Oliver","family":"Kaiser","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]},{"given":"Amin","family":"Timany","sequence":"additional","affiliation":[{"name":"imec-Distrinet, Belgium \/ KU Leuven, Belgium"}]},{"given":"Arthur","family":"Chargu\u00e9raud","sequence":"additional","affiliation":[{"name":"Inria, France \/ University of Strasbourg, France \/ CNRS, France \/ ICube, France"}]},{"given":"Derek","family":"Dreyer","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]}],"member":"320","published-online":{"date-parts":[[2018,7,30]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"Andrew W. Appel. 2006. Tactics for separation logic. Available at http:\/\/www.cs.princeton.edu\/~appel\/papers\/septacs.pdf . Andrew W. Appel. 2006. Tactics for separation logic. Available at http:\/\/www.cs.princeton.edu\/~appel\/papers\/septacs.pdf ."},{"key":"e_1_2_2_2_1","volume-title":"Amortised resource analysis with separation logic. LMCS 7, 2","author":"Atkey Robert","year":"2011","unstructured":"Robert Atkey . 2011. Amortised resource analysis with separation logic. LMCS 7, 2 ( 2011 ). Robert Atkey. 2011. Amortised resource analysis with separation logic. LMCS 7, 2 (2011)."},{"key":"e_1_2_2_3_1","first-page":"315","article-title":"Charge! - A framework for higher-order separation logic in Coq","volume":"7406","author":"Bengtson Jesper","year":"2012","unstructured":"Jesper Bengtson , Jonas Braband Jensen , and Lars Birkedal . 2012 . Charge! - A framework for higher-order separation logic in Coq . In ITP (LNCS) , Vol. 7406. 315 \u2013 331 . Jesper Bengtson, Jonas Braband Jensen, and Lars Birkedal. 2012. Charge! - A framework for higher-order separation logic in Coq. In ITP (LNCS), Vol. 7406. 315\u2013331.","journal-title":"ITP (LNCS)"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30538-5_9"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2018.03.016"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.034"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.30"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9457-5"},{"key":"e_1_2_2_10_1","first-page":"190","article-title":"Bringing order to the separation logic jungle","volume":"10695","author":"Cao Qinxiang","year":"2017","unstructured":"Qinxiang Cao , Santiago Cuellar , and Andrew W. Appel . 2017 . Bringing order to the separation logic jungle . In APLAS (LNCS) , Vol. 10695. 190 \u2013 211 . Qinxiang Cao, Santiago Cuellar, and Andrew W. Appel. 2017. Bringing order to the separation logic jungle. In APLAS (LNCS), Vol. 10695. 190\u2013211.","journal-title":"APLAS (LNCS)"},{"key":"e_1_2_2_11_1","doi-asserted-by":"crossref","unstructured":"Arthur Chargu\u00e9raud. 2011. Characteristic formulae for the verification of imperative programs. In ICFP. 418\u2013430. Arthur Chargu\u00e9raud. 2011. Characteristic formulae for the verification of imperative programs. In ICFP. 418\u2013430.","DOI":"10.1145\/2034574.2034828"},{"key":"e_1_2_2_12_1","unstructured":"Arthur Chargu\u00e9raud. 2018. CFML 2.0. http:\/\/www.chargueraud.org\/softs\/cfml\/ . Arthur Chargu\u00e9raud. 2018. CFML 2.0. http:\/\/www.chargueraud.org\/softs\/cfml\/ ."},{"key":"e_1_2_2_13_1","first-page":"260","article-title":"Temporary read-only permissions for separation logic","volume":"10201","author":"Chargu\u00e9raud Arthur","year":"2017","unstructured":"Arthur Chargu\u00e9raud and Fran\u00e7ois Pottier . 2017 . Temporary read-only permissions for separation logic . In ESOP (LNCS) , Vol. 10201. 260 \u2013 286 . Arthur Chargu\u00e9raud and Fran\u00e7ois Pottier. 2017. Temporary read-only permissions for separation logic. In ESOP (LNCS), Vol. 10201. 260\u2013286.","journal-title":"ESOP (LNCS)"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500592"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.04.040"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_2_2_18_1","first-page":"85","article-title":"A tactic language for the system Coq","volume":"1955","author":"Delahaye David","year":"2000","unstructured":"David Delahaye . 2000 . A tactic language for the system Coq . In LPAR (LNCS) , Vol. 1955. 85 \u2013 95 . David Delahaye. 2000. A tactic language for the system Coq. In LPAR (LNCS), Vol. 1955. 85\u201395.","journal-title":"LPAR (LNCS)"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.10.002"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_13"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_23"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429131"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429105"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_2_26_1","volume-title":"Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Accepted for publication in JFP","author":"Jung Ralf","year":"2018","unstructured":"Ralf Jung , Robbert Krebbers , Jacques-Henri Jourdan , Ale\u0161 Bizjak , Lars Birkedal , and Derek Dreyer . 2018b. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Accepted for publication in JFP ( 2018 ). Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ale\u0161 Bizjak, Lars Birkedal, and Derek Dreyer. 2018b. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Accepted for publication in JFP (2018)."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_2_28_1","first-page":"1","article-title":"Strong logic for weak memory: Reasoning about release-acquire consistency in Iris","volume":"74","author":"Kaiser Jan-Oliver","year":"2017","unstructured":"Jan-Oliver Kaiser , Hoang-Hai Dang , Derek Dreyer , Ori Lahav , and Viktor Vafeiadis . 2017 . Strong logic for weak memory: Reasoning about release-acquire consistency in Iris . In ECOOP (LIPIcs) , Vol. 74. 17: 1 \u2013 17 :29. Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. 2017. Strong logic for weak memory: Reasoning about release-acquire consistency in Iris. In ECOOP (LIPIcs), Vol. 74. 17:1\u201317:29.","journal-title":"ECOOP (LIPIcs)"},{"key":"e_1_2_2_30_1","unstructured":"Robbert Krebbers Jacques-Henri Jourdan Ralf Jung Joseph Tassarotti Jan-Oliver Kaiser Amin Timany Arthur Chargu\u00e9raud and Derek Dreyer. 2018. Coq repository for MoSeL. http:\/\/iris- project.org\/mosel\/ . Robbert Krebbers Jacques-Henri Jourdan Ralf Jung Joseph Tassarotti Jan-Oliver Kaiser Amin Timany Arthur Chargu\u00e9raud and Derek Dreyer. 2018. Coq repository for MoSeL. http:\/\/iris- project.org\/mosel\/ ."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_2_33_1","first-page":"264","article-title":"Impartiality, justice and fairness: The ethics of concurrent termination","author":"Lehmann Daniel J.","year":"1981","unstructured":"Daniel J. Lehmann , Amir Pnueli , and Jonathan Stavi . 1981 . Impartiality, justice and fairness: The ethics of concurrent termination . In Automata, Languages and Programming. 264 \u2013 277 . Daniel J. Lehmann, Amir Pnueli, and Jonathan Stavi. 1981. Impartiality, justice and fairness: The ethics of concurrent termination. In Automata, Languages and Programming. 264\u2013277.","journal-title":"Automata, Languages and Programming."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_24"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706331"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/647851.737404"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000366"},{"key":"e_1_2_2_40_1","volume-title":"The semantics and proof theory of the logic of bunched implications","author":"Pym David J.","unstructured":"David J. Pym . 2002. The semantics and proof theory of the logic of bunched implications . Springer . David J. Pym. 2002. The semantics and proof theory of the logic of bunched implications. Springer."},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.11.020"},{"key":"e_1_2_2_42_1","unstructured":"John C. Reynolds. 2000. Intuitionistic reasoning about shared mutable data structure. In Millennial Perspectives in Computer Science. 303\u2013321. John C. Reynolds. 2000. Intuitionistic reasoning about shared mutable data structure. In Millennial Perspectives in Computer Science. 303\u2013321."},{"key":"e_1_2_2_43_1","doi-asserted-by":"crossref","unstructured":"John C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In LICS. 55\u201374. John C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In LICS. 55\u201374.","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737964"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_14"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"e_1_2_2_47_1","first-page":"795","article-title":"Type classes for mathematics in type theory","volume":"21","author":"Spitters Bas","year":"2011","unstructured":"Bas Spitters and Eelis van der Weegen . 2011 . Type classes for mathematics in type theory . MSCS 21 , 4 (2011), 795 \u2013 825 . Bas Spitters and Eelis van der Weegen. 2011. Type classes for mathematics in type theory. MSCS 21, 4 (2011), 795\u2013825.","journal-title":"MSCS"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133913"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_34"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158152"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190234"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_2_2_53_1","first-page":"256","article-title":"A marriage of rely\/guarantee and separation logic","volume":"4703","author":"Vafeiadis Viktor","year":"2007","unstructured":"Viktor Vafeiadis and Matthew J. Parkinson . 2007 . A marriage of rely\/guarantee and separation logic . In CONCUR (LNCS) , Vol. 4703. 256 \u2013 271 . Viktor Vafeiadis and Matthew J. Parkinson. 2007. A marriage of rely\/guarantee and separation logic. In CONCUR (LNCS), Vol. 4703. 256\u2013271.","journal-title":"CONCUR (LNCS)"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3236772","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3236772","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T04:10:10Z","timestamp":1751775010000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3236772"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,30]]},"references-count":52,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2018,7,30]]}},"alternative-id":["10.1145\/3236772"],"URL":"https:\/\/doi.org\/10.1145\/3236772","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,7,30]]},"assertion":[{"value":"2018-07-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}