### Abstract

Commutative Replicated Data Types (CRDTs) are a promising new class of data structures for large-scale shared mutable content in applications that only require eventual consistency. The WithOut Operational Transforms (WOOT) framework is a CRDT for collaborative text editing introduced by Oster et al. (CSCW 2006) for which the eventual consistency property was verified only for a bounded model to date. We contribute a formal proof for WOOTs strong eventual consistency.

### License

BSD License

### Topics

- Computer science/Algorithms/Distributed

### Related publications

- Karayel, E., & Gonzàlez, E. (2022). Strong eventual consistency of the collaborative editing framework WOOT. Distributed Computing, 35(2), 145–164. https://doi.org/10.1007/s00446-021-00414-6

### Session WOOT_Strong_Eventual_Consistency

- ErrorMonad
- Data
- BasicAlgorithms
- CreateAlgorithms
- IntegrateAlgorithm
- DistributedExecution
- SortKeys
- Psi
- Sorting
- Consistency
- CreateConsistent
- IntegrateInsertCommute
- StrongConvergence
- SEC
- Example

### Depends on

- Certification Monads
- Generating linear orders for datatypes

### Auto-related entries

- OpSets: Sequential Specifications for Replicated Datatypes

## Cite

×

WOOT_Strong_Eventual_Consistency-AFP

    @article{WOOT_Strong_Eventual_Consistency-AFP,
      author  = {Emin Karayel and Edgar Gonzàlez},
      title   = {Strong Eventual Consistency of the Collaborative Editing Framework WOOT},
      journal = {Archive of Formal Proofs},
      month   = {March},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/WOOT_Strong_Eventual_Consistency.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 20, 2020 : Isabelle2020
- Mar 26, 2020 : Isabelle2019