{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:28Z","timestamp":1780994668282,"version":"3.54.1"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2021,7,21]],"date-time":"2021-07-21T00:00:00Z","timestamp":1626825600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100003246","name":"Netherlands Organisation for Scientific Research","doi-asserted-by":"crossref","award":["13563"],"award-info":[{"award-number":["13563"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We present a new version of ReLoC: a relational separation logic for proving\nrefinements of programs with higher-order state, fine-grained concurrency,\npolymorphism and recursive types. The core of ReLoC is its refinement judgment\n$e \\precsim e' : \\tau$, which states that a program $e$ refines a program $e'$\nat type $\\tau$. ReLoC provides type-directed structural rules and symbolic\nexecution rules in separation-logic style for manipulating the judgment,\nwhereas in prior work on refinements for languages with higher-order state and\nconcurrency, such proofs were carried out by unfolding the judgment into its\ndefinition in the model. ReLoC's abstract proof rules make it simpler to carry\nout refinement proofs, and enable us to generalize the notion of logically\natomic specifications to the relational case, which we call logically atomic\nrelational specifications.\n  We build ReLoC on top of the Iris framework for separation logic in Coq,\nallowing us to leverage features of Iris to prove soundness of ReLoC, and to\ncarry out refinement proofs in ReLoC. We implement tactics for interactive\nproofs in ReLoC, allowing us to mechanize several case studies in Coq, and\nthereby demonstrate the practicality of ReLoC.\n  ReLoC Reloaded extends ReLoC (LICS'18) with various technical improvements, a\nnew Coq mechanization, and support for Iris's prophecy variables. The latter\nallows us to carry out refinement proofs that involve reasoning about the\nprogram's future. We also expand ReLoC's notion of logically atomic relational\nspecifications with a new flavor based on the HOCAP pattern by Svendsen et al.<\/jats:p>","DOI":"10.46298\/lmcs-17(3:9)2021","type":"journal-article","created":{"date-parts":[[2021,7,27]],"date-time":"2021-07-27T12:15:22Z","timestamp":1627388122000},"source":"Crossref","is-referenced-by-count":21,"title":["ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity"],"prefix":"10.46298","volume":"Volume 17, Issue 3","author":[{"given":"Dan","family":"Frumin","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"25203","published-online":{"date-parts":[[2021,7,21]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/7708\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/7708\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T20:17:56Z","timestamp":1687292276000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/6598"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,7,21]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-17(3:9)2021","relation":{"has-preprint":[{"id-type":"arxiv","id":"2006.13635v2","asserted-by":"subject"},{"id-type":"arxiv","id":"2006.13635v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2006.13635","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2006.13635","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,7,21]]},"article-number":"6598"}}