1: \begin{abstract}

2: 	Replicated data types (RDTs) are data structures that permit concurrent

3: 	modification of multiple, potentially geo-distributed, replicas without

4: 	coordination between them. RDTs are designed in such a way that conflicting

5: 	operations are eventually \emph{deterministically} reconciled ensuring

6: 	\emph{convergence}. Constructing correct RDTs remains a difficult endeavour

7: 	due to the complexity of reasoning about independently evolving states of the

8: 	replicas. With the focus on the correctness of RDTs (and rightly so),

9: 	existing approaches to RDTs are less efficient compared to their sequential

10: 	counterparts in terms of time- and space-complexity of local operations. This

11: 	is unfortunate since RDTs are often used in an local-first setting where the

12: 	local operations far outweigh remote communication.

13: 

14: 	In this paper, we present \name, a pragmatic approach to building and

15: 	verifying efficient RDTs. To make reasoning about correctness easier, we cast

16: 	RDTs in the mould of distributed version control system, and equip it with a

17: 	three-way merge function for reconciling conflicting versions. Further, we go

18: 	beyond just verifying convergence, and provide a methodology to verify

19: 	arbitrarily complex specifications.  We develop a replication-aware

20: 	simulation relation to relate RDT specifications to their efficient purely

21: 	functional implementations. We have developed \name as an F* library that

22: 	discharges proof obligations to an SMT solver. The verified efficient RDTs

23: 	are extracted as OCaml code and used in Irmin, a Git-like distributed

24: 	database.

25: \end{abstract}

26: