{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T06:25:30Z","timestamp":1748413530062},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642226724"},{"type":"electronic","value":"9783642226731"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-22673-1_10","type":"book-chapter","created":{"date-parts":[[2011,7,13]],"date-time":"2011-07-13T07:49:15Z","timestamp":1310543355000},"page":"133-148","source":"Crossref","is-referenced-by-count":22,"title":["Large Formal Wikis: Issues and Solutions"],"prefix":"10.1007","author":[{"given":"Jesse","family":"Alama","sequence":"first","affiliation":[]},{"given":"Kasper","family":"Brink","sequence":"additional","affiliation":[]},{"given":"Lionel","family":"Mamane","sequence":"additional","affiliation":[]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","unstructured":"Alama, J., Mamane, L., Urban, J.: Dependencies in formal mathematics (preprint) (submitted)"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"Intelligent Computer Mathematics","year":"2010","unstructured":"Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.): AISC 2010. LNCS, vol.\u00a06167. Springer, Heidelberg (2010)"},{"issue":"2","key":"10_CR3","first-page":"377","volume":"1","author":"G. Bancerek","year":"1990","unstructured":"Bancerek, G.: Cardinal numbers. Formalized Mathematics\u00a01(2), 377\u2013382 (1990)","journal-title":"Formalized Mathematics"},{"key":"10_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/11812289_21","volume-title":"Mathematical Knowledge Management","author":"G. Bancerek","year":"2006","unstructured":"Bancerek, G.: Information retrieval and rendering with MML Query. In: Borwein, J.M., Farmer, W.M. (eds.) MKM 2006. LNCS (LNAI), vol.\u00a04108, pp. 266\u2013279. Springer, Heidelberg (2006)"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-540-68103-8_5","volume-title":"Types for Proofs and Programs","author":"P. Corbineau","year":"2008","unstructured":"Corbineau, P.: A declarative language for the Coq proof assistant. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2007. LNCS, vol.\u00a04941, pp. 69\u201384. Springer, Heidelberg (2008)"},{"key":"10_CR6","unstructured":"Driessen, V.: A successful Git branching model, \n                    \n                      http:\/\/nvie.com\/posts\/a-successful-git-branching-model\/"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"490","DOI":"10.1007\/978-3-642-14052-5_35","volume-title":"Interactive Theorem Proving","author":"B. Spitters","year":"2010","unstructured":"Spitters, B., van der Weegen, E.: Developing the algebraic hierarchy with type classes in Coq. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 490\u2013493. Springer, Heidelberg (2010)"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Tankink, C., Geuvers, H., McKinna, J., Wiedijk, F.: Proviola: A tool for proof re-animation. In: Autexier, et al. (eds.) [2], pp. 440\u2013454","DOI":"10.1007\/978-3-642-14128-7_37"},{"key":"10_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/11618027_23","volume-title":"Mathematical Knowledge Management","author":"J. Urban","year":"2006","unstructured":"Urban, J.: XML-izing mizar: Making semantic processing and presentation of mml easy. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol.\u00a03863, pp. 346\u2013360. Springer, Heidelberg (2006)"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Urban, J., Alama, J., Rudnicki, P., Geuvers, H.: A wiki for Mizar: Motivation, considerations, and initial prototype. In: Autexier, et al. (eds.) [2], pp. 455\u2013469","DOI":"10.1007\/978-3-642-14128-7_38"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Urban, J., Sutcliffe, G.: Automated reasoning and presentation support for formalizing mathematics in Mizar. In: Autexier, et al. (eds.) [2], pp. 132\u2013146","DOI":"10.1007\/978-3-642-14128-7_12"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22673-1_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,1,25]],"date-time":"2019-01-25T21:50:40Z","timestamp":1548453040000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22673-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642226724","9783642226731"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22673-1_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}