{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:10:08Z","timestamp":1775873408842,"version":"3.50.1"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100008398","name":"VILLUM Foundation","doi-asserted-by":"crossref","award":["25804"],"award-info":[{"award-number":["25804"]}],"id":[{"id":"10.13039\/100008398","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101003349"],"award-info":[{"award-number":["101003349"]}],"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":[[2024,1,2]]},"abstract":"<jats:p>Expressive state-of-the-art separation logics rely on step-indexing to model semantically complex features and to support modular reasoning about imperative higher-order concurrent and distributed programs. Stepindexing comes, however, with an inherent cost: it restricts the adequacy theorem of program logics to a fairly simple class of safety properties.<\/jats:p>\n          <jats:p>\n            In this paper, we explore if and how\n            <jats:italic toggle=\"yes\">intensional refinement<\/jats:italic>\n            is a viable methodology for strengthening higher-order concurrent (and distributed) separation logic to prove non-trivial safety and liveness properties. Specifically, we introduce Trillium, a language-agnostic separation logic framework for showing intensional refinement relations between\n            <jats:italic toggle=\"yes\">traces<\/jats:italic>\n            of a program and a model. We instantiate Trillium with a concurrent language and develop Fairis, a concurrent separation logic, that we use to show liveness properties of concurrent programs under fair scheduling assumptions through a fair liveness-preserving refinement of a model. We also instantiate Trillium with a distributed language and obtain an extension of Aneris, a distributed separation logic, which we use to show refinement relations between distributed systems and TLA\n            <jats:sup>+<\/jats:sup>\n            models.\n          <\/jats:p>","DOI":"10.1145\/3632851","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"241-272","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2237-851X","authenticated-orcid":false,"given":"Amin","family":"Timany","sequence":"first","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6045-5232","authenticated-orcid":false,"given":"Simon Oddershede","family":"Gregersen","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4719-2922","authenticated-orcid":false,"given":"L\u00e9o","family":"Stefanesco","sequence":"additional","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6143-9031","authenticated-orcid":false,"given":"Jonas Kastberg","family":"Hinrichsen","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8262-6397","authenticated-orcid":false,"given":"L\u00e9on","family":"Gondelman","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2741-8119","authenticated-orcid":false,"given":"Abel","family":"Nieto","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1320-0098","authenticated-orcid":false,"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473586"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","unstructured":"Tej Chajed Joseph Tassarotti M. Frans Kaashoek and Nickolai Zeldovich. 2019. Verifying concurrent crash-safe systems with Perennial. In Proceedings of the 27th ACM Symposium on Operating Systems Principles SOSP 2019 Huntsville ON Canada October 27-30 2019. 243\u2013258. https:\/\/doi.org\/10.1145\/3341301.3359632 10.1145\/3341301.3359632","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_8"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044482830-9\/50024-2"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","unstructured":"Dan Frumin Robbert Krebbers and Lars Birkedal. 2018. ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency. In Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science LICS 2018 Oxford UK July 09-12 2018. 442\u2013451. https:\/\/doi.org\/10.1145\/3209108.3209174 10.1145\/3209108.3209174","DOI":"10.1145\/3209108.3209174"},{"key":"e_1_3_1_7_1","article-title":"ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity","volume":"17","author":"Frumin Dan","year":"2020","unstructured":"Dan Frumin, Robbert Krebbers, and Lars Birkedal. 2020. ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity. Log. Methods Comput. Sci. 17 (2020).","journal-title":"Log. Methods Comput. Sci"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498689"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_32"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527318"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-08755-9_9"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","unstructured":"Simon Oddershede Gregersen Alejandro Aguirre Philipp G. Haselwarter Joseph Tassarotti and Lars Birkedal. 2023. Asynchronous Probabilistic Couplings in Higher-Order Separation Logic. CoRR abs\/2301.10061 (2023). https:\/\/doi.org\/10.48550\/arXiv.2301.10061 10.48550\/arXiv.2301.10061 arXiv:2301.10061","DOI":"10.48550\/arXiv.2301.10061"},{"key":"e_1_3_1_13_1","unstructured":"Ronghui Gu J\u00e9r\u00e9mie Koenig Tahina Ramananandro Zhong Shao Xiongnan (Newman) Wu Shu-Chun Weng Haozhong Zhang and Yu Guo. 2015. Deep Specifications and Certified Abstraction Layers. In POPL. ACM."},{"key":"e_1_3_1_14_1","first-page":"653","volume-title":"Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (Savannah, GA, USA) (OSDI\u201916)","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (Savannah, GA, USA) (OSDI\u201916). USENIX Association, USA, 653\u2013669."},{"key":"e_1_3_1_15_1","doi-asserted-by":"crossref","unstructured":"Ronghui Gu Zhong Shao Jieung Kim Xiongnan (Newman) Wu J\u00e9r\u00e9mie Koenig Vilhelm Sj\u00f6berg Hao Chen David Costanzo and Tahina Ramananandro. 2018. Certified concurrent abstraction layers. In PLDI. ACM 646\u2013661.","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3068608"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527326"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434288"},{"key":"e_1_3_1_19_1","unstructured":"Mauro Jaskelioff and Stephan Merz. 2005. Proving the Correctness of Disk Paxos. Arch. Formal Proofs 2005 (2005) https:\/\/www.isa-afp.org\/entries\/DiskPaxos.shtml"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung David Swasey Filip Sieczkowski Kasper Svendsen Aaron Turon Lars Birkedal and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL 2015 Mumbai India January 15-17 2015. 637\u2013650. https:\/\/doi.org\/10.1145\/2676726.2676980 10.1145\/2676726.2676980","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_1_22_1","unstructured":"Pertti Kellom\u00e4ki. 2004. An Annotated Specification of the Consensus Protocol of Paxos Using Superposition in PVS. Technical Report. Tampere University of Technology. Institute of Software Systems."},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385980"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009877"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3030-44914-8_13"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-573186_25"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_3_1_29_1","doi-asserted-by":"crossref","unstructured":"Leslie Lamport. 2001. Paxos Made Simple. ACM SIGACT News (Distributed Computing Column) 32 4 (Whole Number 121 December 2001) (December 2001) 51\u201358.","DOI":"10.1145\/568425.568433"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837635"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","unstructured":"Hongjin Liang and Xinyu Feng. 2018. Progress of concurrent objects with partial methods. Proc. ACM Program. Lang. 2 POPL (2018) 20:1\u201320:31. https:\/\/doi.org\/10.1145\/3158108 10.1145\/3158108","DOI":"10.1145\/3158108"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_12"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140568"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/9783-662-46669-8_7"},{"key":"e_1_3_1_35_1","first-page":"67","article-title":"Convergent and Commutative Replicated Data Types","volume":"104","author":"Shapiro Marc","year":"2011","unstructured":"Marc Shapiro, Nuno M. Pregui\u00e7a, Carlos Baquero, and Marek Zawirski. 2011. Convergent and Commutative Replicated Data Types. Bull. EATCS 104 (2011), 67\u201388. http:\/\/eatcs.org\/beatcs\/index.php\/beatcs\/article\/view\/120","journal-title":"Bull. EATCS"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","unstructured":"Simon Spies Lennard G\u00e4her Daniel Gratzer Joseph Tassarotti Robbert Krebbers Derek Dreyer and Lars Birkedal. 2021. Transfinite Iris: resolving an existential dilemma of step-indexed separation logic. In PLDI \u201921: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation Virtual Event Canada June 20-25 20211. 80\u201395. https:\/\/doi.org\/10.1145\/3453483.3454031 10.1145\/3453483.3454031","DOI":"10.1145\/3453483.3454031"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428220"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290377"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_34"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341709"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","unstructured":"Amin Timany Simon Oddershede Gregersen L\u00e9o Stefanesco Jonas Kastberg Hinrichsen L\u00e9on Gondelman Abel Nieto and Lars Birkedal. 2023. Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement - Coq Artifact. https:\/\/doi.org\/10.5281\/zenodo 10.5281\/zenodo. 10100892","DOI":"10.5281\/zenodo"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158152"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1435417.1435432"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632851","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632851","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:04:58Z","timestamp":1751659498000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632851"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":42,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632851"],"URL":"https:\/\/doi.org\/10.1145\/3632851","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}