{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T23:21:30Z","timestamp":1770247290060,"version":"3.49.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2238744"],"award-info":[{"award-number":["2238744"]}],"id":[{"id":"10.13039\/100000001","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":[[2025,1,7]]},"abstract":"<jats:p>\n                    Version control systems typically rely on a\n                    <jats:italic toggle=\"yes\">patch language<\/jats:italic>\n                    , heuristic\n                    <jats:italic toggle=\"yes\">patch synthesis algorithms<\/jats:italic>\n                    like\n                    <jats:monospace>diff<\/jats:monospace>\n                    , and\n                    <jats:italic toggle=\"yes\">three-way merge algorithms<\/jats:italic>\n                    . Standard patch languages and merge algorithms often fail to identify conflicts correctly when there are multiple edits to one line of code or code is relocated. This paper introduces Grove, a collaborative structure editor calculus that eliminates patch synthesis and three-way merge algorithms entirely. Instead, patches are derived directly from the log of the developer\u2019s edit actions and all edits commute, i.e. the repository state forms a commutative replicated data type (CmRDT). To handle conflicts that can arise due to code relocation, the core datatype in Grove is a labeled directed multi-graph with uniquely identified vertices and edges. All edits amount to edge insertion and deletion, with deletion being permanent. To support tree-based editing, we define a decomposition from graphs into\n                    <jats:italic toggle=\"yes\">groves<\/jats:italic>\n                    , which are a set of syntax trees with conflicts\u2013including local, relocation, and unicyclic relocation conflicts\u2013represented explicitly using holes and references between trees. Finally, we define a type error localization system for groves that enjoys a\n                    <jats:italic toggle=\"yes\">totality<\/jats:italic>\n                    property, i.e. all editor states in Grove are statically meaningful, so developers can use standard editor services while working to resolve these explicitly represented conflicts. The static semantics is defined as a bidirectional marking system in line with recent work, with gradual typing employed to handle situations where errors and conflicts prevent type determination. We then layer on a unification-based type inference system to opportunistically fill type holes and fail gracefully when no solution exists. We mechanize the metatheory of Grove using the Agda theorem prover. We implement these ideas as the\n                    <jats:italic toggle=\"yes\">Grove Workbench<\/jats:italic>\n                    , which generates the necessary data structures and algorithms in OCaml given a syntax tree specification.\n                  <\/jats:p>","DOI":"10.1145\/3704909","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"2176-2204","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3160-6972","authenticated-orcid":false,"given":"Michael D.","family":"Adams","sequence":"first","affiliation":[{"name":"National University of Singapore, Singapore, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1693-6172","authenticated-orcid":false,"given":"Eric","family":"Griffis","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-1809-8382","authenticated-orcid":false,"given":"Thomas J.","family":"Porter","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-8685-1342","authenticated-orcid":false,"given":"Sundara Vishnu","family":"Satish","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-4969-2376","authenticated-orcid":false,"given":"Eric","family":"Zhao","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4502-7971","authenticated-orcid":false,"given":"Cyrus","family":"Omar","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","unstructured":"Michael Adams Eric Griffis Thomas Porter Sundara Vishnu Satish Eric Zhao and Cyrus Omar.2024. Artifact for Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus. https:\/\/doi.org\/10.5281\/zenodo.14026532 10.5281\/zenodo.14026532","DOI":"10.5281\/zenodo.14026532"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/2034691.2034717"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000198"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2010-282"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2004.12.030"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/253260.253266"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/1644015.1644017"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3450952"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/67544.66963"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/2642937.2642982"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2007.70731"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/1832772.1832777"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002864"},{"key":"e_1_3_2_15_2","unstructured":"James W. Hunt and M. Douglas McIlroy. 1976. An Algorithm for Differential File Comparison. (1976). https:\/\/www.cs.dartmouth.edu\/%7Edoug\/diff.pdf"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1002\/CPE.4110"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-68530-8_8"},{"key":"e_1_3_2_18_2","first-page":"1","article-title":"Moving elements in list CRDTs","author":"Kleppmann Martin","year":"2020","unstructured":"Martin Kleppmann. 2020. Moving elements in list CRDTs. In Proceedings of the 7th Workshop on Principles and Practice of Consistency for Distributed Data. 1\u20136.","journal-title":"Proceedings of the 7th Workshop on Principles and Practice of Consistency for Distributed Data"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2021.3118603"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/1030397.1030399"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3555644"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/1868358.1868363"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/2494266.2494278"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12029-9_6"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/2957276.2957310"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","unstructured":"Cyrus Omar Ian Voysey Michael Hilton Jonathan Aldrich and Matthew A. Hammer. 2017. Hazelnut: a bidirectionally typed structure editor calculus. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages POPL 2017 Paris France January 18-20 2017 Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM 86\u201399. https:\/\/doi.org\/10.1145\/3009837.3009900 10.1145\/3009837.3009900","DOI":"10.1145\/3009837.3009900"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","unstructured":"Cyrus Omar Ian Voysey Michael Hilton Joshua Sunshine Claire Le Goues Jonathan Aldrich and Matthew A. Hammer. 2017. Toward Semantic Foundations for Program Editors. In 2nd Summit on Advances in Programming Languages SNAPL 2017 May 7-10 2017 Asilomar CA USA (LIPIcs Vol. 71) BenjaminS. Lerner Rastislav Bodik and Shriram Krishnamurthi (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik 11:1\u201311:12. https:\/\/doi.org\/10.4230\/LIPICS.SNAPL.2017.11 10.4230\/LIPICS.SNAPL.2017.11","DOI":"10.4230\/LIPICS.SNAPL.2017.11"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/1180875.1180916"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1109\/5.771073"},{"key":"e_1_3_2_30_2","article-title":"Conflict-free replicated data types (CRDTs)","author":"Pregui\u00e7a Nuno","year":"2018","unstructured":"Nuno Pregui\u00e7a, Carlos Baquero, and Marc Shapiro. 2018. Conflict-free replicated data types (CRDTs). arXiv preprint arXiv:1805.06358 (2018).","journal-title":"arXiv preprint arXiv:1805.06358"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICDCS.2009.20"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.JPDC.2010.12.006"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/1088348.1088349"},{"key":"e_1_3_2_34_2","unstructured":"David Roundy. 2009. Darcs2.1.0.1 Appendix A: Theory of patches. https:\/\/www.cs.tufts.edu\/comp\/150GIT\/archive\/david-roundy\/theory-patches-2009.pdf"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2015.02.008"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24550-3_29"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","unstructured":"Jeremy G. Siek Michael M. Vitousek Matteo Cimini and John Tang Boyland. 2015. Refined Criteria for Gradual Typing. In 1st Summit on Advances in Programming Languages SNAPL 2015 May 3-6 2015 Asilomar California USA (LIPIcs Vol. 32) Thomas Ball Rastislav Bodik Shriram Krishnamurthi Benjamin S. Lerner and Greg Morrisett (Eds.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik 274\u2013293. https:\/\/doi.org\/10.4230\/LIPICS.SNAPL.2015.274 10.4230\/LIPICS.SNAPL.2015.274","DOI":"10.4230\/LIPICS.SNAPL.2015.274"},{"key":"e_1_3_2_38_2","unstructured":"Nathan Sobo. 2022. How CRDTs make multiplayer text editing part of Zed's DNA. https:\/\/zed.dev\/blog\/crdts"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_3"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/358746.358755"},{"key":"e_1_3_2_41_2","first-page":"383","volume-title":"International Summer School on Generative and Transformational Techniques in Software Engineering","author":"Voelter Markus","year":"2011","unstructured":"Markus Voelter. 2011. Language and IDE Modularization and Composition with MPS. In International Summer School on Generative and Transformational Techniques in Software Engineering. Springer, 383\u2013430."},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1002\/SPE.2187"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICDCS.2009.75"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632910"},{"key":"e_1_3_2_45_2","unstructured":"Pierre \u00c9tienne Meunier. 2024. Version control post-Git. FOSDEM 2024. https:\/\/archive.fosdem.org\/2024\/schedule\/event\/fosdem-2024-3423-version-control-post-git\/"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704909","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704909","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:17:12Z","timestamp":1770200232000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704909"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":44,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704909"],"URL":"https:\/\/doi.org\/10.1145\/3704909","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}