{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,25]],"date-time":"2026-09-25T09:55:42Z","timestamp":1790330142055,"version":"4.1.0"},"reference-count":67,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100004837","name":"Ministerio de Ciencia e Innovaci\u00f3n","doi-asserted-by":"crossref","award":["PGC2018-102210-B-I00"],"award-info":[{"award-number":["PGC2018-102210-B-I00"]}],"id":[{"id":"10.13039\/501100004837","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100011199","name":"European Research Council","doi-asserted-by":"publisher","award":["ERC2016-COG-724464"],"award-info":[{"award-number":["ERC2016-COG-724464"]}],"id":[{"id":"10.13039\/100011199","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":[[2019,10,10]]},"abstract":"<jats:p>\n            In addition to pre- and postconditions, program specifications in recent separation logics for concurrency have employed an algebraic structure of\n            <jats:italic>resources<\/jats:italic>\n            \u2014a form of state transition systems\u2014to describe the state-based program invariants that must be preserved, and to record the permissible atomic changes to program state. In this paper we introduce a novel notion of\n            <jats:italic>resource morphism<\/jats:italic>\n            , i.e.\u00a0structure-preserving function on resources, and show how to effectively integrate it into separation logic, using an associated notion of morphism-specific\n            <jats:italic>simulation<\/jats:italic>\n            . We apply morphisms and simulations to programs verified under one resource, to compositionally adapt them to operate under another resource, thus facilitating proof reuse.\n          <\/jats:p>","DOI":"10.1145\/3360587","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Specifying concurrent programs in separation logic: morphisms and simulations"],"prefix":"10.1145","volume":"3","author":[{"given":"Aleksandar","family":"Nanevski","sequence":"first","affiliation":[{"name":"IMDEA Software Institute, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Anindya","family":"Banerjee","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Germ\u00e1n Andr\u00e9s","family":"Delbianco","sequence":"additional","affiliation":[{"name":"IRIF, France \/ University of Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ignacio","family":"F\u00e1bregas","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.272.9"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/185675.185815"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_26"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9_9"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040327"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_28"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.034"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43951-7_9"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/362759.362813"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/503271.503226"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.8"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1889997.1890001"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.021"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-009-0125-8"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209174"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290316"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/b978-1-4832-0016-3.50006-8"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_19"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03741-2_6"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1810479.1810540"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40184-8_18"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1108\/03684920810907904"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-6315-9_16"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/cbo9781316823187"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926417"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43951-7_19"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_24"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429134"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462189"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158108"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103711"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603123"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1134"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/103727.103729"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_2_2_47_1","series-title":"Lecture Notes for the Oregon Programming Languages Summer School (OPLSS). https:\/\/www.cs.uoregon.edu\/research\/summerschool\/summer16\/curriculum.php","volume-title":"Separation Logic and Concurrency","author":"Nanevski Aleksandar","unstructured":"Aleksandar Nanevski . 2016. Separation Logic and Concurrency . Lecture Notes for the Oregon Programming Languages Summer School (OPLSS). https:\/\/www.cs.uoregon.edu\/research\/summerschool\/summer16\/curriculum.php Aleksandar Nanevski. 2016. Separation Logic and Concurrency. Lecture Notes for the Oregon Programming Languages Summer School (OPLSS). https:\/\/www.cs.uoregon.edu\/research\/summerschool\/summer16\/curriculum.php"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.3365991"},{"key":"e_1_2_2_49_1","volume-title":"Germ\u00e1n Andr\u00e9s Delbianco, and Ignacio F\u00e1bregas","author":"Nanevski Aleksandar","year":"2019","unstructured":"Aleksandar Nanevski , Anindya Banerjee , Germ\u00e1n Andr\u00e9s Delbianco, and Ignacio F\u00e1bregas . 2019 b. Specifying Concurrent Programs in Separation Logic : Morphisms and Simulations . (2019). arXiv: 1904.07136 Aleksandar Nanevski, Anindya Banerjee, Germ\u00e1n Andr\u00e9s Delbianco, and Ignacio F\u00e1bregas. 2019b. Specifying Concurrent Programs in Separation Logic: Morphisms and Simulations. (2019). arXiv: 1904.07136"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_16"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159812"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411237"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/lics.2001.932499"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1016\/s0304-3975(00)00056-6"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_21"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737964"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_14"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022671.2983999"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158116"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21691-6_17"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_11"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544174.2500600"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360587","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360587","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:59Z","timestamp":1750202579000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360587"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":67,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360587"],"URL":"https:\/\/doi.org\/10.1145\/3360587","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}