Standard

Verified operational transformation for trees. / Sinchuk, Sergey; Chuprikov, Pavel; Solomatov, Konstantin.

Interactive Theorem Proving - 7th International Conference, ITP 2016, Proceedings. ред. / Jasmin Christian Blanchette; Stephan Merz. Springer Nature, 2016. стр. 358-373 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Том 9807 LNCS).

Результаты исследований: Публикации в книгах, отчётах, сборниках, трудах конференций › статья в сборнике материалов конференции › Рецензирование

Harvard

Sinchuk, S, Chuprikov, P & Solomatov, K 2016, Verified operational transformation for trees. в JC Blanchette & S Merz (ред.), 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), Том. 9807 LNCS, Springer Nature, стр. 358-373, 7th International Conference on Interactive Theorem Proving, ITP 2016, Nancy, Франция, 22/08/16. https://doi.org/10.1007/978-3-319-43144-4_22

APA

Sinchuk, S., Chuprikov, P., & Solomatov, K. (2016). Verified operational transformation for trees. в J. C. Blanchette, & S. Merz (Ред.), Interactive Theorem Proving - 7th International Conference, ITP 2016, Proceedings (стр. 358-373). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Том 9807 LNCS). Springer Nature. https://doi.org/10.1007/978-3-319-43144-4_22

Vancouver

Sinchuk S, Chuprikov P, Solomatov K. Verified operational transformation for trees. в Blanchette JC, Merz S, Редакторы, Interactive Theorem Proving - 7th International Conference, ITP 2016, Proceedings. Springer Nature. 2016. стр. 358-373. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-43144-4_22

Author

Sinchuk, Sergey ; Chuprikov, Pavel ; Solomatov, Konstantin. / Verified operational transformation for trees. Interactive Theorem Proving - 7th International Conference, ITP 2016, Proceedings. Редактор / Jasmin Christian Blanchette ; Stephan Merz. Springer Nature, 2016. стр. 358-373 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

BibTeX

@inproceedings{8cd90b3fc0a54a8f9f31ae0b5635bb2d,
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",
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 Nature",
pages = "358--373",
editor = "Blanchette, {Jasmin Christian} and Stephan Merz",
booktitle = "Interactive Theorem Proving - 7th International Conference, ITP 2016, Proceedings",
address = "Germany",
note = "7th International Conference on Interactive Theorem Proving, ITP 2016 ; Conference date: 22-08-2016 Through 25-08-2016",

}

RIS

TY - GEN

T1 - Verified operational transformation for trees

AU - Sinchuk, Sergey

AU - Chuprikov, Pavel

AU - Solomatov, Konstantin

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 - http://www.scopus.com/inward/record.url?scp=84984783313&partnerID=8YFLogxK

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 Nature

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

Y2 - 22 August 2016 through 25 August 2016

ER -

ID: 36088772