The IMAP CmRDT

Tim Jungnickel 📧, Lennart Oldenburg and Matthias Loibl

November 9, 2017

Abstract

We provide our Isabelle/HOL formalization of a Conflict-free Replicated Datatype for Internet Message Access Protocol commands. We show that Strong Eventual Consistency (SEC) is guaranteed by proving the commutativity of concurrent operations. We base our formalization on the recently proposed "framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes" (AFP.CRDT) from Gomes et al. Hence, we provide an additional example of how the recently proposed framework can be used to design and prove CRDTs.

License

BSD License

Topics

Session IMAP-CRDT