Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP article: Strong Eventual Consistency o...

view this post on Zulip Email Gateway (Aug 23 2022 at 08:32):

From: Tobias Nipkow <nipkow@in.tum.de>
Strong Eventual Consistency of the Collaborative Editing Framework WOOT
Emin Karayel and Edgar Gonzàlez

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.

https://www.isa-afp.org/entries/WOOT_Strong_Eventual_Consistency.html

Enjoy!
smime.p7s

Last updated: Apr 24 2024 at 04:17 UTC