### 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

- Computer science/Algorithms/Distributed
- Computer science/Data structures

### Session IMAP-CRDT

- IMAP-def
- IMAP-proof-commute
- IMAP-proof-helpers
- IMAP-proof-independent
- IMAP-proof

### Depends on

- A framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes

## Cite

×

IMAP-CRDT-AFP

    @article{IMAP-CRDT-AFP,
      author  = {Tim Jungnickel and Lennart Oldenburg and Matthias Loibl},
      title   = {The IMAP CmRDT},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/IMAP-CRDT.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jan 14, 2020 : Isabelle2019
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Nov 10, 2017 : Isabelle2017