| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
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{http://isa-afp.org/entries/IMAP-CRDT.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | CRDT |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |