{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T08:34:07Z","timestamp":1791189247636,"version":"4.1.0"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319089690","type":"print"},{"value":"9783319089706","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08970-6_30","type":"book-chapter","created":{"date-parts":[[2014,6,28]],"date-time":"2014-06-28T11:13:26Z","timestamp":1403954006000},"page":"467-482","source":"Crossref","is-referenced-by-count":7,"title":["Collaborative Interactive Theorem Proving with Clide"],"prefix":"10.1007","author":[{"given":"Martin","family":"Ring","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christoph","family":"L\u00fcth","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"30_CR1","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-642-39320-4_22","volume-title":"Intelligent Computer Mathematics","author":"C. L\u00fcth","year":"2013","unstructured":"L\u00fcth, C., Ring, M.: A web interface for Isabelle: The next generation. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol.\u00a07961, pp. 326\u2013329. Springer, Heidelberg (2013)"},{"key":"30_CR2","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"468","DOI":"10.1007\/978-3-642-31374-5_38","volume-title":"Intelligent Computer Mathematics","author":"M. Wenzel","year":"2012","unstructured":"Wenzel, M.: Isabelle\/jEdit \u2013 A prover IDE within the PIDE framework. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS (LNAI), vol.\u00a07362, pp. 468\u2013471. Springer, Heidelberg (2012)"},{"key":"30_CR3","unstructured":"ProofPeer web page, \n                    \n                      http:\/\/www.proofpeer.net\n                    \n                    \n                   (accessed: January 29, 2014)"},{"key":"30_CR4","doi-asserted-by":"crossref","unstructured":"Dourish, P., Bellotti, V.: Awareness and coordination in shared workspaces. In: Proceedings of the 1992 ACM Conference on Computer-supported Cooperative Work, CSCW 1992, pp. 107\u2013114. ACM (1992)","DOI":"10.1145\/143457.143468"},{"issue":"1","key":"30_CR5","doi-asserted-by":"publisher","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.\u00a05(1), 63\u2013108 (1998)","journal-title":"ACM Trans. Comput.-Hum. Interact."},{"issue":"2","key":"30_CR6","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1145\/66926.66963","volume":"18","author":"C.A. Ellis","year":"1989","unstructured":"Ellis, C.A., Gibbs, S.J.: Concurrency control in groupware systems. SIGMOD Rec.\u00a018(2), 399\u2013407 (1989)","journal-title":"SIGMOD Rec."},{"key":"30_CR7","unstructured":"Wang, D., Mah, A., Lassen, S.: Google Wave operational transformation, \n                    \n                      http:\/\/www.waveprotocol.org\/whitepapers\/operational-transform\/operational-transform.html\n                    \n                    \n                   (accessed: January 30, 2014)"},{"key":"30_CR8","unstructured":"Haftmann, F., Nipkow, T.: A code generator framework for Isabelle\/HOL. In: Theorem Proving in Higher Order Logics (TPHOLs 2007), Emerging Trends Proceedings, Dept. of Computer Science, University of Kaiserslautern, pp. 128\u2013143 (2007)"},{"key":"30_CR9","unstructured":"Doeraene, S.: Scala.js website, \n                    \n                      http:\/\/www.scala-js.org\n                    \n                    \n                   (accessed: January 29, 2014)"},{"key":"30_CR10","unstructured":"Typesafe Inc.: Typesafe reactive platform overview, \n                    \n                      http:\/\/typesafe.com\/platform\n                    \n                    \n                   (accessed: January 29, 2014)"},{"key":"30_CR11","unstructured":"Wyatt, D.: Akka Concurrency. Artima Press (2013)"},{"key":"30_CR12","doi-asserted-by":"crossref","unstructured":"Greenberg, S., Marwood, D.: Real time groupware as a distributed system: Concurrency control and its effect on the interface. In: Proc. ACM 1994 Conference on Computer Supported Cooperative Work, CSCW 1994, pp. 207\u2013217. ACM (1994)","DOI":"10.1145\/192844.193011"},{"key":"30_CR13","doi-asserted-by":"crossref","unstructured":"Sun, C., Ellis, C.: Operational transformation in real-time group editors: Issues, algorithms, and achievements. In: Proc. 1998 ACM Conference on Computer Supported Cooperative Work, CSCW 1998, pp. 59\u201368. ACM (1998)","DOI":"10.1145\/289444.289469"},{"key":"30_CR14","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C.: Web interfaces for proof assistants. In: Autexier, S., Benzm\u00fcller, C. (eds.) Proc. of the Workshop on User Interfaces for Theorem Provers (UITP 2006). ENTCS, vol.\u00a0174(2), pp. 49\u201361 (2007)","DOI":"10.1016\/j.entcs.2006.09.021"},{"key":"30_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/978-3-642-14128-7_38","volume-title":"Intelligent Computer Mathematics","author":"J. Urban","year":"2010","unstructured":"Urban, J., Alama, J., Rudnicki, P., Geuvers, H.: A wiki for Mizar: Motivation, considerations, and initial prototype. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC 2010. LNCS, vol.\u00a06167, pp. 455\u2013469. Springer, Heidelberg (2010)"},{"key":"30_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-642-22673-1_10","volume-title":"Intelligent Computer Mathematics","author":"J. Alama","year":"2011","unstructured":"Alama, J., Brink, K., Mamane, L., Urban, J.: Large formal wikis: Issues and solutions. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Calculemus\/MKM 2011. LNCS, vol.\u00a06824, pp. 133\u2013148. Springer, Heidelberg (2011)"},{"key":"30_CR17","doi-asserted-by":"crossref","unstructured":"Tankink, C.: Proof in context \u2014 web editing with rich, modeless contextual feedback. In: Kaliszyk, C., L\u00fcth, C. (eds.) Proc. 10th International Workshop on User Interfaces for Theorem Provers (UITP 2012). EPTCS, vol.\u00a0118, pp. 42\u201356 (2013)","DOI":"10.4204\/EPTCS.118.3"},{"key":"30_CR18","doi-asserted-by":"crossref","unstructured":"Komendantskaya, E., Heras, J., Grov, G.: Machine learning in Proof General: Interfacing interfaces. In: Kaliszyk, C., L\u00fcth, C. (eds.) Proceedings 10th International Workshop on User Interfaces for Theorem Provers, UITP 2012. EPTCS, vol.\u00a0118, pp. 15\u201341 (2013)","DOI":"10.4204\/EPTCS.118.2"},{"key":"30_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/11618027_5","volume-title":"Mathematical Knowledge Management","author":"D. Aspinall","year":"2006","unstructured":"Aspinall, D., L\u00fcth, C., Wolff, B.: Assisted proof document authoring. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol.\u00a03863, pp. 65\u201380. Springer, Heidelberg (2006)"}],"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-08970-6_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T05:18:59Z","timestamp":1558934339000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08970-6_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319089690","9783319089706"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08970-6_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}