DOI

Operational transformation (OT) is an approach to concurrency control in groupware editors first proposed by C. Ellis and S. Gibbs in 1989. Google Wave and Google Docs are examples of better known OT-based systems and there are many other experimental ones described in the literature. In their recent articles A. Imine et al. have shown that many OT implementations contain mistakes and do not possess claimed consistency properties. The present work describes an experimental library which is based on SSReflect/Coq and contains several operational transformation algorithms and proofs of their correctness.

Original languageEnglish
Title of host publicationInteractive Theorem Proving - 7th International Conference, ITP 2016, Proceedings
EditorsJasmin Christian Blanchette, Stephan Merz
PublisherSpringer Nature
Pages358-373
Number of pages16
ISBN (Print)9783319431437
DOIs
StatePublished - 1 Jan 2016
Event7th International Conference on Interactive Theorem Proving, ITP 2016 - Nancy, France
Duration: 22 Aug 2016 → 25 Aug 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9807 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference7th International Conference on Interactive Theorem Proving, ITP 2016
Country/TerritoryFrance
CityNancy
Period22/08/16 → 25/08/16

    Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

ID: 36088772