The IMAP CmRDT

 

Title: The IMAP CmRDT
Authors: Tim Jungnickel (tim /dot/ jungnickel /at/ tu-berlin /dot/ de), Lennart Oldenburg and Matthias Loibl
Submission date: 2017-11-09
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.
BibTeX:
@article{IMAP-CRDT-AFP,
  author  = {Tim Jungnickel and Lennart Oldenburg and Matthias Loibl},
  title   = {The IMAP CmRDT},
  journal = {Archive of Formal Proofs},
  month   = nov,
  year    = 2017,
  note    = {\url{https://isa-afp.org/entries/IMAP-CRDT.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: CRDT