{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:36Z","timestamp":1774837836637,"version":"3.50.1"},"publisher-location":"Cham","reference-count":14,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319221014","type":"print"},{"value":"9783319221021","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-22102-1_4","type":"book-chapter","created":{"date-parts":[[2015,8,18]],"date-time":"2015-08-18T08:30:14Z","timestamp":1439886614000},"page":"51-66","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface"],"prefix":"10.1007","author":[{"given":"Bruno","family":"Barras","sequence":"first","affiliation":[]},{"given":"Carst","family":"Tankink","sequence":"additional","affiliation":[]},{"given":"Enrico","family":"Tassi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,8,19]]},"reference":[{"issue":"1","key":"4_CR1","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/s12046-009-0003-3","volume":"34","author":"A Asperti","year":"2009","unstructured":"Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: A compact kernel for the calculus of inductive constructions. Sadhana 34(1), 71\u2013144 (2009)","journal-title":"Sadhana"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/3-540-46419-0_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Aspinall","year":"2000","unstructured":"Aspinall, D.: Proof general: a generic tool for proof development. In: Graf, S. (ed.) TACAS 2000. LNCS, vol. 1785, pp. 38\u201342. Springer, Heidelberg (2000)"},{"key":"4_CR3","unstructured":"Bengtson, J., Mehnert, H., Faithfull, A.: Coqoon: eclipse plugin providing a feature-complete development environment for Coq (2015). Homepage: https:\/\/itu.dk\/research\/tomeso\/coqoon\/"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Faithfull, A., Tankink, C., Bengtson, J.: Coqoon - an IDE for interactive proof development in Coq. Submitted to CAV 2015","DOI":"10.1007\/978-3-662-49674-9_18"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-39634-2_14","volume-title":"Interactive Theorem Proving","author":"G Gonthier","year":"2013","unstructured":"Gonthier, G., et al.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 163\u2013179. Springer, Heidelberg (2013)"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Hayes, B.: Ephemerons: a new finalization mechanism. In: Proceedings of OOPSLA, pp. 176\u2013183. ACM (1997)","DOI":"10.1145\/263700.263733"},{"issue":"6","key":"4_CR7","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1743546.1743574","volume":"53","author":"G Klein","year":"2010","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an operating-system kernel. Commun. ACM 53(6), 107\u2013115 (2010)","journal-title":"Commun. ACM"},{"issue":"7","key":"4_CR8","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"4_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL: A Proof Assistant for Higher-order Logic. Springer, Heidelberg (2002)"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1007\/978-3-319-08970-6_30","volume-title":"Interactive Theorem Proving","author":"M Ring","year":"2014","unstructured":"Ring, M., L\u00fcth, C.: Collaborative interactive theorem proving with clide. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 467\u2013482. Springer, Heidelberg (2014)"},{"key":"4_CR11","unstructured":"Wenzel, M.: Parallel proof checking in Isabelle\/Isar. In: Proceedings of PLMMS, pp. 13\u201321 (2009)"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-22673-1_17","volume-title":"Intelligent Computer Mathematics","author":"M Wenzel","year":"2011","unstructured":"Wenzel, M.: Isabelle as document-oriented proof assistant. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Calculemus\/MKM 2011. LNCS, vol. 6824, pp. 244\u2013259. Springer, Heidelberg (2011)"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: READ-EVAL-PRINT in parallel and asynchronous proof-checking. In: Proceedings of UITP. EPTCS, vol. 118, pp. 57\u201371 (2013)","DOI":"10.4204\/EPTCS.118.4"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"515","DOI":"10.1007\/978-3-319-08970-6_33","volume-title":"Interactive Theorem Proving","author":"M Wenzel","year":"2014","unstructured":"Wenzel, M.: Asynchronous user interaction and tool integration in Isabelle\/PIDE. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 515\u2013530. Springer, Heidelberg (2014)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-22102-1_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,20]],"date-time":"2023-01-20T18:37:50Z","timestamp":1674239870000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-22102-1_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319221014","9783319221021"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-22102-1_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"19 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}