{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:48:00Z","timestamp":1780994880698,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":62,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,6,18]],"date-time":"2021-06-18T00:00:00Z","timestamp":1623974400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100008398","name":"Villum Fonden","doi-asserted-by":"publisher","award":["25804"],"award-info":[{"award-number":["25804"]}],"id":[{"id":"10.13039\/100008398","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003246","name":"Nederlandse Organisatie voor Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","award":["016.Veni.192.259"],"award-info":[{"award-number":["016.Veni.192.259"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["683289"],"award-info":[{"award-number":["683289"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,6,19]]},"DOI":"10.1145\/3453483.3454031","type":"proceedings-article","created":{"date-parts":[[2021,6,18]],"date-time":"2021-06-18T13:51:32Z","timestamp":1624024292000},"page":"80-95","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":27,"title":["Transfinite Iris: resolving an existential dilemma of step-indexed separation logic"],"prefix":"10.1145","author":[{"given":"Simon","family":"Spies","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany \/ Saarland University, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lennard","family":"G\u00e4her","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany \/ Saarland University, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Daniel","family":"Gratzer","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joseph","family":"Tassarotti","sequence":"additional","affiliation":[{"name":"Boston College, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Derek","family":"Dreyer","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1320-0098","authenticated-orcid":false,"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,6,18]]},"reference":[{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029818"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480925"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(89)90027-5"},{"key":"e_1_3_2_1_5_1","volume-title":"Program Logics for Certified Compilers","author":"Appel Andrew W.","unstructured":"Andrew W. Appel , Robert Dockins , Aquinas Hobor , Lennart Beringer , Josiah Dodds , Gordon Stewart , Sandrine Blazy , and Xavier Leroy . 2014. Program Logics for Certified Compilers . Cambridge University Press . isbn:110704801X Andrew W. Appel, Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. 2014. Program Logics for Certified Compilers. Cambridge University Press. isbn:110704801X"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_6"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434283"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:4)2013"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.16"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926401"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08918-8_8"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90098-9"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9457-5"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034828"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_8"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371102"},{"key":"e_1_3_2_1_21_1","volume-title":"Controlling and Reasoning About State (Dagstuhl Seminar Proceedings","author":"Dockins Robert","year":"2010","unstructured":"Robert Dockins and Aquinas Hobor . 2010 . A theory of termination via indirection. In Modelling , Controlling and Reasoning About State (Dagstuhl Seminar Proceedings , Vol. 10351). http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2010\/2805\/ Robert Dockins and Aquinas Hobor. 2010. A theory of termination via indirection. In Modelling, Controlling and Reasoning About State (Dagstuhl Seminar Proceedings, Vol. 10351). http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2010\/2805\/"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2012.08.010"},{"key":"e_1_3_2_1_23_1","unstructured":"Emanuele D\u2019Osualdo Azadeh Farzan Philippa Gardner and Julian Sutherland. 2019. TaDA Live: Compositional reasoning for termination of fine-grained concurrent programs. arxiv:1901.05750  Emanuele D\u2019Osualdo Azadeh Farzan Philippa Gardner and Julian Sutherland. 2019. TaDA Live: Compositional reasoning for termination of fine-grained concurrent programs. arxiv:1901.05750"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:16)2011"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706323"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209174"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Dan Frumin Robbert Krebbers and Lars Birkedal. 2021. Compositional non-interference for fine-grained concurrent programs. To appear in S&P\u201921.  Dan Frumin Robbert Krebbers and Lars Birkedal. 2021. Compositional non-interference for fine-grained concurrent programs. To appear in S&P\u201921.","DOI":"10.1109\/SP40001.2021.00003"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24727-2_11"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408996"},{"key":"e_1_3_2_1_30_1","unstructured":"Gerhard Hessenberg. 1906. Grundbegriffe der Mengenlehre. 1 Vandenhoeck & Ruprecht.  Gerhard Hessenberg. 1906. Grundbegriffe der Mengenlehre. 1 Vandenhoeck & Ruprecht."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78739-6_27"},{"key":"e_1_3_2_1_32_1","unstructured":"Iris project. 2021. A higher-order concurrent separation logic framework implemented and verified in the proof assistant Coq. https:\/\/iris-project.org\/  Iris project. 2021. A higher-order concurrent separation logic framework implemented and verified in the proof assistant Coq. https:\/\/iris-project.org\/"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3418295"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167095"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009855"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009877"},{"key":"e_1_3_2_1_44_1","first-page":"707","article-title":"Binary codes capable of correcting deletions, insertions, and reversals","volume":"10","author":"Levenshtein Vladimir Iosifovich","year":"1965","unstructured":"Vladimir Iosifovich Levenshtein . 1965 . Binary codes capable of correcting deletions, insertions, and reversals . Soviet Physics Doklady , 10 (1965), 707 \u2013 710 . Vladimir Iosifovich Levenshtein. 1965. Binary codes capable of correcting deletions, insertions, and reversals. Soviet Physics Doklady, 10 (1965), 707\u2013710.","journal-title":"Soviet Physics Doklady"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837635"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158108"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_1"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408978"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2000.855774"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_2_1_52_1","unstructured":"Simon Spies Lennard G\u00e4her Daniel Gratzer Joseph Tassarotti Robbert Krebbers Derek Dreyer and Lars Birkedal. 2021. Transfinite Iris appendix and Coq development. https:\/\/iris-project.org\/transfinite-iris\/  Simon Spies Lennard G\u00e4her Daniel Gratzer Joseph Tassarotti Robbert Krebbers Derek Dreyer and Lars Birkedal. 2021. Transfinite Iris appendix and Coq development. https:\/\/iris-project.org\/transfinite-iris\/"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434294"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_11"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_13"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_28"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_34"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158152"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429111"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014566"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71389-0_26"}],"event":{"name":"PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"Virtual Canada","acronym":"PLDI '21","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3453483.3454031","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3453483.3454031","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:03:07Z","timestamp":1750197787000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3453483.3454031"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,18]]},"references-count":62,"alternative-id":["10.1145\/3453483.3454031","10.1145\/3453483"],"URL":"https:\/\/doi.org\/10.1145\/3453483.3454031","relation":{},"subject":[],"published":{"date-parts":[[2021,6,18]]},"assertion":[{"value":"2021-06-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}