{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T18:52:27Z","timestamp":1773168747845,"version":"3.50.1"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2019,7,26]],"date-time":"2019-07-26T00:00:00Z","timestamp":1564099200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-15-2-0096"],"award-info":[{"award-number":["FA8750-15-2-0096"]}],"id":[{"id":"10.13039\/100000185","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,7,26]]},"abstract":"<jats:p>\n            We introduce Carol, a refinement-typed programming language for replicated data stores. The salient feature of Carol is that it allows programming and verifying replicated store operations\n            <jats:italic>modularly<\/jats:italic>\n            , without consideration of other operations that might interleave, and\n            <jats:italic>sequentially<\/jats:italic>\n            , without requiring reference to or knowledge of the concurrent execution model. This is in stark contrast with existing systems, which require understanding the concurrent interactions of all pairs of operations when developing or verifying them.\n          <\/jats:p>\n          <jats:p>\n            The key enabling idea is the\n            <jats:italic>consistency guard<\/jats:italic>\n            , a two-state predicate relating the locally-viewed store and the hypothetical remote store that an operation\u2019s updates may eventually be applied to, which is used by the Carol programmer to declare their precise consistency requirements. Guards appear to the programmer and refinement typechecker as simple data pre-conditions, enabling sequential reasoning, while appearing to the distributed runtime as consistency control instructions.\n          <\/jats:p>\n          <jats:p>We implement and evaluate the Carol system in two parts: (1) the algorithm used to statically translate guards into the runtime coordination actions required to enforce them, and (2) the networked-replica runtime which executes arbitrary operations, written in a Haskell DSL, according to the Carol language semantics.<\/jats:p>","DOI":"10.1145\/3341710","type":"journal-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:55:51Z","timestamp":1564433751000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Sequential programming for replicated data stores"],"prefix":"10.1145","volume":"3","author":[{"given":"Nicholas V.","family":"Lewchenko","sequence":"first","affiliation":[{"name":"University of Colorado Boulder, USA"}]},{"given":"Arjun","family":"Radhakrishna","sequence":"additional","affiliation":[{"name":"Microsoft, USA"}]},{"given":"Akash","family":"Gaonkar","sequence":"additional","affiliation":[{"name":"University of Colorado Boulder, USA"}]},{"given":"Pavol","family":"\u010cern\u00fd","sequence":"additional","affiliation":[{"name":"University of Colorado Boulder, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,7,26]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933057.2933090"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2463676.2465279"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.14778\/3297753.3297760"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2741948.2741972"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/343477.343502"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000011"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_4"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535848"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/564585.564601"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2011.389"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837625"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276534"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1773912.1773922"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/2643634.2643664"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/2387880.2387906"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2723372.2723720"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.713327"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/2050613.2050642"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737981"},{"key":"e_1_2_2_23_1","unstructured":"Pedro Teixeira. 2017. Decentralized Real-Time Collaborative Documents - Conflict-free editing in the browser using js-ipfs and CRDTs. https:\/\/ipfs.io\/blog\/30-js-ipfs-crdts.md .  Pedro Teixeira. 2017. Decentralized Real-Time Collaborative Documents - Conflict-free editing in the browser using js-ipfs and CRDTs. https:\/\/ipfs.io\/blog\/30-js-ipfs-crdts.md ."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522731"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/224056.224070"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277732"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341710","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341710","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341710","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:24Z","timestamp":1750207404000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341710"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,26]]},"references-count":27,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2019,7,26]]}},"alternative-id":["10.1145\/3341710"],"URL":"https:\/\/doi.org\/10.1145\/3341710","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,7,26]]},"assertion":[{"value":"2019-07-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}