Verified operational transformation for trees

Sergey Sinchuk; Pavel Chuprikov; Konstantin Solomatov

doi:10.1007/978-3-319-43144-4_22

Verified operational transformation for trees

Sergey Sinchuk, Pavel Chuprikov, Konstantin Solomatov

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

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 language	English
Title of host publication	Interactive Theorem Proving - 7th International Conference, ITP 2016, Proceedings
Editors	Jasmin Christian Blanchette, Stephan Merz
Publisher	Springer Verlag
Pages	358-373
Number of pages	16
ISBN (Print)	9783319431437
DOIs	https://doi.org/10.1007/978-3-319-43144-4_22
Publication status	Published - 1 Jan 2016
Externally published	Yes
Event	7th International Conference on Interactive Theorem Proving, ITP 2016 - Nancy, France Duration: 22 Aug 2016 → 25 Aug 2016

Publication series

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

Conference

Conference	7th International Conference on Interactive Theorem Proving, ITP 2016
Country/Territory	France
City	Nancy
Period	22/08/16 → 25/08/16

Access to Document

10.1007/978-3-319-43144-4_22

Cite this

Sinchuk, S., Chuprikov, P., & Solomatov, K. (2016). Verified operational transformation for trees. In J. C. Blanchette, & S. Merz (Eds.), Interactive Theorem Proving - 7th International Conference, ITP 2016, Proceedings (pp. 358-373). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9807 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-43144-4_22

Sinchuk, Sergey ; Chuprikov, Pavel ; Solomatov, Konstantin. / Verified operational transformation for trees. Interactive Theorem Proving - 7th International Conference, ITP 2016, Proceedings. editor / Jasmin Christian Blanchette ; Stephan Merz. Springer Verlag, 2016. pp. 358-373 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{17e22261d64e4b5b97006acca9fa18b9,

title = "Verified operational transformation for trees",

abstract = "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.",

author = "Sergey Sinchuk and Pavel Chuprikov and Konstantin Solomatov",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2016.; 7th International Conference on Interactive Theorem Proving, ITP 2016 ; Conference date: 22-08-2016 Through 25-08-2016",

year = "2016",

month = jan,

day = "1",

doi = "10.1007/978-3-319-43144-4\_22",

language = "English",

isbn = "9783319431437",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "358--373",

editor = "Blanchette, \{Jasmin Christian\} and Stephan Merz",

booktitle = "Interactive Theorem Proving - 7th International Conference, ITP 2016, Proceedings",

}

Sinchuk, S, Chuprikov, P & Solomatov, K 2016, Verified operational transformation for trees. in JC Blanchette & S Merz (eds), Interactive Theorem Proving - 7th International Conference, ITP 2016, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9807 LNCS, Springer Verlag, pp. 358-373, 7th International Conference on Interactive Theorem Proving, ITP 2016, Nancy, France, 22/08/16. https://doi.org/10.1007/978-3-319-43144-4_22

Verified operational transformation for trees. / Sinchuk, Sergey; Chuprikov, Pavel; Solomatov, Konstantin.
Interactive Theorem Proving - 7th International Conference, ITP 2016, Proceedings. ed. / Jasmin Christian Blanchette; Stephan Merz. Springer Verlag, 2016. p. 358-373 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9807 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Verified operational transformation for trees

AU - Sinchuk, Sergey

AU - Chuprikov, Pavel

AU - Solomatov, Konstantin

N1 - Publisher Copyright: © Springer International Publishing Switzerland 2016.

PY - 2016/1/1

Y1 - 2016/1/1

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/84984783313

U2 - 10.1007/978-3-319-43144-4_22

DO - 10.1007/978-3-319-43144-4_22

M3 - Conference contribution

AN - SCOPUS:84984783313

SN - 9783319431437

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 358

EP - 373

BT - Interactive Theorem Proving - 7th International Conference, ITP 2016, Proceedings

A2 - Blanchette, Jasmin Christian

A2 - Merz, Stephan

PB - Springer Verlag

T2 - 7th International Conference on Interactive Theorem Proving, ITP 2016

Y2 - 22 August 2016 through 25 August 2016

ER -

Sinchuk S, Chuprikov P, Solomatov K. Verified operational transformation for trees. In Blanchette JC, Merz S, editors, Interactive Theorem Proving - 7th International Conference, ITP 2016, Proceedings. Springer Verlag. 2016. p. 358-373. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-43144-4_22

Verified operational transformation for trees

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this