Implementation Correctness for Replicated Data Types, Categorically

Replicated Data Types (rdts) have been introduced as an abstraction for dealing with weakly consistent data stores, which may (temporarily) expose multiple, inconsistent views of their state. In the literature, rdts are usually presented in set-theoretical terms: Only recently different specification flavours have been proposed, among them a denotational formalism that inter alia captures specification refinement. So far, however, no abstract model has been proposed for the implementations and their correctness with respect to specifications. This paper fills the gap: We first give categorical constructions for distilling an operational model from a specification, as well as its implementations, and then we define a notion of implementation correctness via simulation.