Conflict-free Replicated Data Types (CRDTs) are modern distributed data types that allow replicating data to different devices in a distributed system and enable local copies to diverge until they are merged with other replicas ensuring eventual consistency. CRDTs play a vital role in building local-first applications, i.e., applications where devices can always progress their local state independently while also enabling seamless collaboration among devices without being blocked by devices that are (temporarily) unreachable on the network. CRDTs enable keeping replicated data consistent while guaranteeing the absence of conflicts among replicas. CRDTs come in two flavors: state-based and operation-based (op-based). For correct operation, state-based CRDTs rely on a merge function for two states that is commutative, associative and idempotent, while operation-based CRDTs rely on an application function for operations on the state that commutes with itself.
However ensuring that such algebraic properties are satisfied by implementations is left to the programmer, resulting in a process that is complex and error-prone. While techniques based on testing, automatic verification of models, and mechanized or handwritten proofs are available, we lack an approach that is able to verify such properties on concrete CRDT implementations.
In this talk the first author will present the first type system that captures the algebraic properties required by a correct CRDT implementation. The type system is designed in Propel, it can reason about programs and derive proofs of such properties with complex rules such as case analysis and induction: sum types guide the case analysis and algebraic properties in function types enable induction. Propel’s key feature is its capacity to reason about algebraic properties (a) in terms of rewrite rules and (b) to derive the equality or inequality of expressions from the properties.
