Categorical specification and implementation of Replicated Data Types

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, and only recently different specification flavours have been proposed. This paper offers a categorical presentation for the specification and implementation of RDTs. This paves the way for a method that allows distilling an operational semantics from a specification, which is then exploited to define a notion of implementation correctness via simulation.