This Sunday we're hosting Alexander Städing to present Composing CRDTs Convergent by Construction, joint work with George Zakhour, Pascal Weisenburger, and Guido Salvaneschi. Conflict-Free Replicated Data Types let copies of shared data accept updates without central coordination and still arrive at the same state. That makes them useful for collaborative editors, offline-capable applications, and distributed databases. The trouble begins when an application needs more than one of them:
Classical CRDT theory does not guarantee that a composition of convergent CRDTs converges.
Their answer is a basis of five combinators for operation-based CRDTs. Product updates two component states together; MapState changes a CRDT's internal representation; Associate builds maps whose values are themselves CRDTs; Traverse expands one operation into a sequence of operations; and MapInterpretation changes the value exposed to the application. In the Crdtlib implementation, every CRDT carries its commutativity proof as part of its Lean structure, and every combinator constructs that proof for its output. A well-typed composition therefore brings its convergence argument with it.
The authors test the framework at three scales: rebuilding standard CRDTs, modeling a collaborative tic-tac-toe game with branching histories and chat, and constructing a JSON-like tree with nested maps, lists, scalars, and counters. The last case offers an interface comparable to Automerge and remains competitive in the paper's runtime and memory benchmarks. Because the model, proofs, and implementation are all written in Lean 4, the machine-checked artifact is also the code that runs.
Alex will begin with the 20-minute OOPSLA conference presentation, then spend the rest of the 45-minute session walking through the Lean code. Join us at The Pearl House this Sunday, September 6; the meetup begins at 2:00 PM and the talk begins at 2:30 PM.