{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:46:34Z","timestamp":1780994794446,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":28,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,7,9]],"date-time":"2018-07-09T00:00:00Z","timestamp":1531094400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100003246","name":"Nederlandse Organisatie voor Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","award":["STW-14319"],"award-info":[{"award-number":["STW-14319"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100008394","name":"Natur og Univers, Det Frie Forskningsr\u00e5d","doi-asserted-by":"publisher","award":["12-133344"],"award-info":[{"award-number":["12-133344"]}],"id":[{"id":"10.13039\/100008394","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,7,9]]},"DOI":"10.1145\/3209108.3209174","type":"proceedings-article","created":{"date-parts":[[2018,6,27]],"date-time":"2018-06-27T12:14:43Z","timestamp":1530101683000},"page":"442-451","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":45,"title":["ReLoC"],"prefix":"10.1145","author":[{"given":"Dan","family":"Frumin","sequence":"first","affiliation":[{"name":"Radboud University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[{"name":"Delft University of Technology"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,7,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110265"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Amal Ahmed Andrew W. Appel and Roberto Virga. 2002. A stratified semantics of general references embeddable in higher-order logic. In LICS. 75--86. Amal Ahmed Andrew W. Appel and Roberto Virga. 2002. A stratified semantics of general references embeddable in higher-order logic. In LICS. 75--86.","DOI":"10.1109\/LICS.2002.1029818"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480925"},{"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","first-page":"1","article-title":"Relational logic with framing and hypotheses","volume":"65","author":"Banerjee Anindya","year":"2016","unstructured":"Anindya Banerjee , David A. Naumann , and Mohammad Nikouei . 2016 . Relational logic with framing and hypotheses . In FSTTCS (LIPIcs) , Vol. 65. 11: 1 -- 11 :16. Anindya Banerjee, David A. Naumann, and Mohammad Nikouei. 2016. Relational logic with framing and hypotheses. In FSTTCS (LIPIcs), Vol. 65. 11:1--11:16.","journal-title":"FSTTCS (LIPIcs)"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2485982"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926401"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_3_2_1_12_1","first-page":"504","article-title":"Concurrent abstract predicates","volume":"6183","author":"Dinsdale-Young Thomas","year":"2010","unstructured":"Thomas Dinsdale-Young , Mike Dodds , Philippa Gardner , Matthew J. Parkinson , and Viktor Vafeiadis . 2010 . Concurrent abstract predicates . In ECOOP (LNCS) , Vol. 6183. 504 -- 528 . Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, and Viktor Vafeiadis. 2010. Concurrent abstract predicates. In ECOOP (LNCS), Vol. 6183. 504--528.","journal-title":"ECOOP (LNCS)"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.34"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681200024X"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706323"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Dan Frumin Robbert Krebbers and Lars Birkedal. 2018. Appendix and Coq development of ReLoC: A mechanised relational logic for fine-grained concurrency. (2018). Available at http:\/\/cs.ru.nl\/~dfrumin\/reloc\/. Dan Frumin Robbert Krebbers and Lars Birkedal. 2018. Appendix and Coq development of ReLoC: A mechanised relational logic for fine-grained concurrency. (2018). Available at http:\/\/cs.ru.nl\/~dfrumin\/reloc\/.","DOI":"10.1145\/3209108.3209174"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926417"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_3_2_1_20_1","volume-title":"Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Submitted for publication","author":"Jung Ralf","year":"2017","unstructured":"Ralf Jung , Robbert Krebbers , Jacques-Henri Jourdan , Ale\u0161 Bizjak , Lars Birkedal , and Derek Dreyer . 2017. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Submitted for publication ( 2017 ). Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ale\u0161 Bizjak, Lars Birkedal, and Derek Dreyer. 2017. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Submitted for publication (2017)."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462189"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491522.2491523"},{"key":"e_1_3_2_1_26_1","first-page":"361","article-title":"A logic for parametric polymorphism","volume":"664","author":"Plotkin Gordon D.","year":"1993","unstructured":"Gordon D. Plotkin and Mart\u00edn Abadi . 1993 . A logic for parametric polymorphism . In TLCA (LNCS) , Vol. 664. 361 -- 375 . Gordon D. Plotkin and Mart\u00edn Abadi. 1993. A logic for parametric polymorphism. In TLCA (LNCS), Vol. 664. 361--375.","journal-title":"TLCA (LNCS)"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.036"}],"event":{"name":"LICS '18: 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science","location":"Oxford United Kingdom","acronym":"LICS '18","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","EACSL European Association for Computer Science Logic","IEEE-CS\\DATC IEEE Computer Society"]},"container-title":["Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3209108.3209174","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3209108.3209174","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T11:02:38Z","timestamp":1751713358000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3209108.3209174"}},"subtitle":["A Mechanised Relational Logic for Fine-Grained Concurrency"],"short-title":[],"issued":{"date-parts":[[2018,7,9]]},"references-count":28,"alternative-id":["10.1145\/3209108.3209174","10.1145\/3209108"],"URL":"https:\/\/doi.org\/10.1145\/3209108.3209174","relation":{},"subject":[],"published":{"date-parts":[[2018,7,9]]},"assertion":[{"value":"2018-07-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}