{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:21:32Z","timestamp":1740097292293,"version":"3.37.3"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319431437"},{"type":"electronic","value":"9783319431444"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-43144-4_22","type":"book-chapter","created":{"date-parts":[[2016,8,6]],"date-time":"2016-08-06T00:24:16Z","timestamp":1470443056000},"page":"358-373","source":"Crossref","is-referenced-by-count":4,"title":["Verified Operational Transformation for Trees"],"prefix":"10.1007","author":[{"given":"Sergey","family":"Sinchuk","sequence":"first","affiliation":[]},{"given":"Pavel","family":"Chuprikov","sequence":"additional","affiliation":[]},{"given":"Konstantin","family":"Solomatov","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,8,7]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/9153.001.0001","volume-title":"Certified Programming with Dependent Types","author":"A Chlipala","year":"2013","unstructured":"Chlipala, A.: Certified Programming with Dependent Types. The MIT press, Cambridge (2013)"},{"key":"22_CR2","unstructured":"Cormack, G.: A counterexample to the distributed operational transform and a corrected algorithm for point-to-point communication. Technical report, CS-95-06, Univ. Waterloo (1995). http:\/\/cs.uwaterloo.ca\/research\/tr\/1995\/08\/dopt.pdf"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"Davis, A.H., Sun, C., Lu, J.: Generalizing operational transformation to the standard general markup language. In: Proceedings of Computer Supported Cooperative Work, pp. 58\u201367 (2002). http:\/\/dx.doi.org\/10.1145\/587078.587088","DOI":"10.1145\/587078.587088"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Ellis, C., Gibbs, S.: Concurrency control in groupware systems. In: Proceedings of 1989 ACM SIGMOD International Conference on Management of Data, vol. 18, pp. 399\u2013407 (1989). http:\/\/dx.doi.org\/10.1145\/66926.66963","DOI":"10.1145\/66926.66963"},{"key":"22_CR5","unstructured":"Gonthier, G., Mahboubi, A., Tassi, E.: A Small Scale Reflection Extension for the Coq system. Research Report RR-6455, Inria Saclay Ile de France (2015). https:\/\/hal.inria.fr\/inria-00258384"},{"key":"22_CR6","unstructured":"Ignat, C.L., Norrie, M.C.: Customizable collaborative editor relying on treeOPT algorithm. In: Proceedings of 8th European Conference Computer Supported Cooperative Work, ECSCW 2003, pp. 315\u2013334 (2003). http:\/\/citeseer.ist.psu.edu\/viewdoc\/download?doi=10.1.1.70.9273&rep=rep1&type=pdf"},{"issue":"2","key":"22_CR7","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1016\/j.tcs.2005.09.066","volume":"351","author":"A Imine","year":"2006","unstructured":"Imine, A., Rusinowitch, M., Molli, P., Oster, G.: Formal design and verification of operational transformation for copies convergence. Theor. Comput. Sci. 351(2), 167\u2013183 (2006). http:\/\/dx.doi.org\/10.1016\/j.tcs.2005.09.066","journal-title":"Theor. Comput. Sci."},{"issue":"6","key":"22_CR8","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1016\/S0020-0190(03)00227-8","volume":"86","author":"B Lushman","year":"2003","unstructured":"Lushman, B., Cormack, G.V.: Proof of correctness of Ressel\u2019s adOPTed algorithm. Inform. Process. Lett. 86(6), 303\u2013310 (2003). http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0020019003002278","journal-title":"Inform. Process. Lett."},{"key":"22_CR9","unstructured":"Lushman, B., Roegist, A.: An automated verication of property tp2 for concurrent collaborative text buffers. Technical report, CS-2012-25, Univ. Waterloo, December 2012. http:\/\/cs.uwaterloo.ca\/sites\/ca.computer-science\/files\/uploads\/files\/CS-2012-25.pdf"},{"key":"22_CR10","doi-asserted-by":"crossref","first-page":"45","DOI":"10.4204\/EPTCS.107.5","volume":"107","author":"A Randolph","year":"2013","unstructured":"Randolph, A., Boucheneb, H., Imine, A., Quintero, A.: On consistency of operational transformation approach. Elec. Proc. Theor. Comput. Sci. 107, 45\u201359 (2013). http:\/\/dx.doi.org\/10.4204\/EPTCS.107.5","journal-title":"Elec. Proc. Theor. Comput. Sci."},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Suleiman, M., Cart, M., Ferri\u00e9, J.: Concurrent operations in a distributed and mobile collaborative environment. In: Proceedings of 14th International Conference Data Engineering, Orlando, FL, USA, 23\u201327 February, pp. 36\u201345 (1998). http:\/\/dx.doi.org\/10.1109\/ICDE.1998.655755","DOI":"10.1109\/ICDE.1998.655755"},{"key":"22_CR12","unstructured":"Sun, C.: Operational transformation frequently asked questions and answers (2010). http:\/\/cooffice.ntu.edu.sg\/otfaq\/"},{"issue":"1","key":"22_CR13","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1145\/274444.274447","volume":"5","author":"C Sun","year":"1998","unstructured":"Sun, C., Jia, X., Zhang, Y., Yang, Y., Chen, D.: Achieving convergence, causality preservation, and intention preservation in real-time cooperative editing systems. ACM Trans. Comput. Hum. Interact. 5(1), 63\u2013108 (1998). http:\/\/dx.doi.org\/10.1145\/274444.274447","journal-title":"ACM Trans. Comput. Hum. Interact."}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-43144-4_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,12]],"date-time":"2019-09-12T03:37:32Z","timestamp":1568259452000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-43144-4_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319431437","9783319431444"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-43144-4_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}