Type-Checking CRDT Convergence
summary
Propel is a Scala-embedded language and type system that encodes CRDT merge laws as types and automatically proves them by case analysis, induction, and rewrite rules. The implementation compiles to JavaScript, verifies 20 open-source CRDTs and discharges 91 properties (commutativity, associativity, idempotence, selectivity and some relational laws), and outperforms four state‑of‑the‑art verification tools on these benchmarks, producing machine-checked proofs without manual lemma-writing.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:47Eventual consistency and CRDTs
- 3:34CRDT convergence examples
- 6:42CRDT correctness challenges
- 7:24Typed CRDT verification
- 8:27Typed CRDT implementation
- 12:36Evaluation vs tools
- 13:38Summary and tools
- 14:00Q&A
related talks
17mMixed & Verified Consistency with Propel and ConOpY
01h 30mImplementing, verifying and debugging distributed event-based systems
22mKatara: Synthesizing CRDTs with Verified Lifting
14mAutomatically Verifying Replication-aware Linearizability
40mPractical Demystification of CRDT
14mBolt-On Strong Consistency: Specification, Implementation, and Verification
33mProgramming Support for Local-First Software
29mAbout Combining Functional Reactive Programming and Replicated Data Types