Composing CRDTs Convergent by Construction

Composing CRDTs Convergent by Construction (SPLASH 2026 - OOPSLA) - SPLASH 2026

SPLASH 2026Sat 3 - Fri 9 October 2026 Oakland, California, United States co-located with SPLASH/ISSTA 2026

Toggle navigation Attending Hotel: Oakland Marriott City Center SPLASH/ISSTA 2026 Visa Letter Registration Travel and Child Care Support Grants

Tracks SPLASH 2026 OOPSLA Onward! Essays Onward! Papers Onward! Steering Committee SIGPLAN track SPLASH Keynotes SPLASH/OOPSLA @ 40 Panel SPLASH-E Artifact evaluation SPLASH/ISSTA 2026 Doctoral symposium PLMW @ SPLASH/ISSTA'26 Posters Social Events Student Research Competition Student Volunteers Summer School Tool Demonstrations REBASE industry track Workshops Sponsorship

Co-hosted Conferences ISSTA ISSTA ISSTA Research papers ISSTA Artifact evaluation ISSTA Keynotes

Workshops EXPRESS Expression of software system DevOps FTA Firmware Testing and Analysis HATRA IWACO LMPL NSAD PLSS PL Standardization and Specification SpecOps Specification-Driven Development Life Cycle SSNL VMIL Co-hosted Symposia SAS Static Analysis SymposiumSAS SAS Artifact

Organization SPLASH 2026 Committees Track Committees OOPSLA Onward! Essays Onward! Papers Onward! Steering Committee SIGPLAN track SPLASH/OOPSLA @ 40 Panel SPLASH-E Artifact evaluation SPLASH/ISSTA Doctoral symposium PLMW @ SPLASH/ISSTA'26 Posters Social Events Student Research Competition Student Volunteers Summer School Speakers Organizers

Tool Demonstrations REBASE industry track Workshops Sponsorship Contributors People Index

Co-hosted Conferences ISSTA Research papers Artifact evaluation

Workshops EXPRESS Expression of software system DevOpsOrganizing Committee Steering Committee Program Committee

FTA Organizing Committee Program Committee

HATRA Organizing Committee Program Committee

IWACO Organizing Committee

LMPL Keynote Speaker Organizing Committee Program Committee

NSAD Organizing Committee Program Committee Steering Committee

PLSS PL Standardization and SpecificationOrganizers

SpecOps Specification-Driven Development Life CycleProgram Committee

SSNL N/A - check homepage

VMIL Program Committee

Co-hosted Symposia SAS Static Analysis SymposiumSAS 2026 Program Committee SAS 2026 Steering Committee SAS Artifact

Search Series Series

SPLASH 2027 SPLASH 2026 SPLASH 2025 SPLASH 2024 SPLASH 2023 SPLASH 2022 SPLASH 2021 SPLASH 2020 SPLASH 2019 SPLASH 2018 SPLASH 2017 SPLASH 2016 SPLASH 2015 SPLASH 2014 SPLASH 2013 SPLASH 2012 SPLASH 2011

SPLASH 2010

OOPSLA 2009 OOPSLA 2008 OOPSLA 2007 OOPSLA 2006 OOPSLA 2005 OOPSLA 2004 OOPSLA 2003 OOPSLA 2002 OOPSLA 2001 OOPSLA 2000

SPLASH/ISSTA 2026 (series) / SPLASH 2026 (series) / OOPSLA / Composing CRDTs Convergent by Construction

WhoAlexander Städing Dominguez, George Zakhour, Pascal Weisenburger, Guido Salvaneschi

TrackSPLASH 2026 OOPSLA

AbstractConflict-Free Replicated Data Types (CRDTs) are abstract data types that ensure eventual convergence among data replicas in distributed systems. As they provide convergence out-of-the-box, CRDTs have become key building blocks for highly available, collaborative, and offline-capable systems, powering applications from real-time editors to distributed databases. Adopting an individual CRDT is straightforward, but real-world software routinely requires composing them. For example, an application might store a set of counters, combining a set CRDT with a counter CRDT. Unfortunately, classical CRDT theory does not guarantee that a composition of convergent CRDTs converges, forcing developers to reason about convergence again - the very burden CRDTs were introduced to remove.

In this paper, we introduce a compositional framework for a broad class of operation-based CRDTs. It assembles CRDTs from five principal combinators – Product, MapState, Associate, Traverse, and MapInterpretation – each with built-in convergence guarantees. Any CRDT assembled from these combinators is itself a CRDT, preserving convergence by construction. This set is free of redundancy and subsumes previously proposed combinators.

We develop the framework, its underlying theory, and its proofs entirely in Lean 4, producing a single artifact that serves as both the formal model and an executable, verified implementation. Our reusable library, Crdtlib, provides implementations and proofs for every combinator and CRDT in this paper. Our case studies (i) implement common CRDTs from Shapiro et al., (ii) apply the combinators in a complete application, and (iii) encode a JSON-structured tree CRDT as expressive as Automerge, with competitive runtime and memory use. These case studies show that developers can compose CRDTs without re-proving convergence for each composite.

Link to Preprint https://programming-group.com/assets/pdf/papers/2026_Composing_CRDTs_Convergent_by_Construction.pdf

DOI https://doi.org/10.1145/3839478

Alexander Städing Dominguez University of St. Gallen Switzerland

George Zakhour University of St. Gallen Switzerland

Pascal...

Composing CRDTs Convergent by Construction

Related Articles

Incident with Github.com

(no title)

Scientists reverse brain aging, with a nasal spray

NHS apologises and admits Palantir have access to identifiable patient data

Cursor Origin