POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States
Thu 23 Jan 2025 11:20 - 11:40 at Peek-A-Boo - Syntax and Editing Chair(s): Guido Salvaneschi

Version control systems typically rely on a \emph{patch language}, heuristic \emph{patch synthesis algorithms} like diff, and \emph{three-way merge algorithms}. 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’s 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 \emph{groves}, which are a set of syntax trees with conflicts—including local, relocation, and unicyclic relocation conflicts— represented explicitly using holes and references between trees. Finally, we define a type error localization system for groves that enjoys a \emph{totality} 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 \emph{Grove Workbench}, which generates the necessary data structures and algorithms in OCaml given a syntax tree specification.

Thu 23 Jan

Displayed time zone: Mountain Time (US & Canada) change

10:40 - 12:00
Syntax and EditingPOPL at Peek-A-Boo
Chair(s): Guido Salvaneschi University of St. Gallen
10:40
20m
Talk
RE#: High Performance Derivative-Based Regex Matching with Intersection, Complement and Restricted Lookarounds
POPL
Ian Erik Varatalu Tallinn University of Technology, Estonia, Margus Veanes Microsoft Research, Juhan Ernits Tallinn University of Technology
DOI Media Attached
11:00
20m
Talk
Pantograph: A Fluid and Typed Structure Editor
POPL
Jacob Prinz University of Maryland, College Park, Henry Blanchette , Leonidas Lampropoulos University of Maryland, College Park
Pre-print Media Attached
11:20
20m
Talk
Grove: A Bidirectionally Typed Collaborative Structure Editor Calculus
POPL
Michael D. Adams National University of Singapore, Eric Griffis University of Michigan, Thomas J. Porter University of Michigan, Sundara Vishnu Satish University of Michigan - Ann Arbor, Eric Zhao Brown University, Cyrus Omar University of Michigan
11:40
20m
Talk
Biparsers: Exact Printing for Data Synchronisation
POPL
Ruifeng Xie Peking University, Tom Schrijvers KU Leuven, Zhenjiang Hu Peking University