@InProceedings{10.1007/978-3-319-43144-4_22,
author="Sinchuk, Sergey
and Chuprikov, Pavel
and Solomatov, Konstantin",
editor="Blanchette, Jasmin Christian
and Merz, Stephan",
title="Verified Operational Transformation for Trees",
booktitle="Interactive Theorem Proving",
year="2016",
publisher="Springer International Publishing",
address="Cham",
pages="358--373",
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.",
isbn="978-3-319-43144-4"
}