ICFP 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025
Wed 15 Oct 2025 11:15 - 11:40 at Orchid Plenary Ballroom - Parametricity Chair(s): Philip Wadler

Conflict-free replicated data types (CRDTs) are distributed data structures designed for fault tolerance and high availability. CRDTs have historically been
taxonomized into \emph{state-based} CRDTs, in which replicas apply updates locally and periodically broadcast their state to other replicas over the network, and \emph{operation-based} (or \emph{op-based}) CRDTs, in which every state-updating operation is individually broadcast. In the literature, state-based and op-based CRDTs are considered equivalent due to the existence of algorithms that let them emulate each other, and verification techniques and results that apply to one kind of CRDT are said to apply to the other thanks to this equivalence. However, what it means for state-based and op-based CRDTs to emulate each other has never been made fully precise. Emulation is nontrivial since state-based and op-based CRDTs place different requirements on the underlying network with regard to both the causal ordering of message delivery, and the granularity of the messages themselves.

We specify and formalize CRDT emulation in terms of \emph{simulation} by modeling CRDTs and their interactions with the network as transition systems. We show that emulation can be understood as \emph{weak simulations} between the transition systems of the original and emulating CRDT systems, thus closing a gap in the CRDT literature. We precisely characterize which properties of CRDT systems are preserved by our weak simulations, and therefore which properties can be said to be preserved by emulation algorithms. Finally, we leverage our emulation results to obtain a general \emph{representation independence} result for CRDTs: intuitively, clients of a CRDT cannot tell whether they are interacting with a state-based or op-based CRDT in particular.

Wed 15 Oct

Displayed time zone: Perth change

10:50 - 12:05
ParametricityICFP Papers / JFP First Papers at Orchid Plenary Ballroom
Chair(s): Philip Wadler IOG; University of Edinburgh
10:50
25m
Talk
A Bargain for Mergesorts: How to Prove Your Mergesort Correct and Stable, Almost for Free
ICFP Papers
Cyril Cohen Inria - CNRS - ENS Lyon - Université Claude Bernard Lyon 1 - LIP - UMR 5668, Kazuhiko Sakaguchi CNRS - ENS Lyon - Université Claude Bernard Lyon 1 - LIP - UMR 5668
DOI Pre-print Media Attached
11:15
25m
Talk
CRDT Emulation, Simulation, and Representation Independence
ICFP Papers
Nathan Liittschwager University of California, Santa Cruz, Jonathan Castello University of California, Santa Cruz, Stelios Tsampas University of Southern Denmark, Lindsey Kuper University of California, Santa Cruz
DOI Pre-print
11:40
25m
Paper
How much is in a square? Calculating functional programs with squares
JFP First Papers
Jose Nuno Oliveira University of Minho; INESC TEC
DOI