{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:12:19Z","timestamp":1775790739772,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642141270","type":"print"},{"value":"9783642141287","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14128-7_37","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T10:45:36Z","timestamp":1277808336000},"page":"440-454","source":"Crossref","is-referenced-by-count":17,"title":["Proviola: A Tool for Proof Re-animation"],"prefix":"10.1007","author":[{"given":"Carst","family":"Tankink","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Herman","family":"Geuvers","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James","family":"McKinna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Freek","family":"Wiedijk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"37_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-540-73086-6_15","volume-title":"Towards Mechanized Mathematical Assistants","author":"D. Aspinall","year":"2007","unstructured":"Aspinall, D., L\u00fcth, C., Winterstein, D.: A framework for interactive proof. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM\/CALCULEMUS 2007. LNCS (LNAI), vol.\u00a04573, pp. 161\u2013175. Springer, Heidelberg (2007)"},{"key":"37_CR2","unstructured":"Coq-Club Mailing List: The Coq-Club mailing list. Mailing List, http:\/\/logical.saclay.inria.fr\/coq-puma\/topics"},{"key":"37_CR3","unstructured":"Coq Development Team, T.: The Coq standard library. Library documented on, http:\/\/coq.inria.fr\/stdlib (obtained on March 5, 2010)"},{"key":"37_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-3-540-73086-6_19","volume-title":"Towards Mechanized Mathematical Assistants","author":"P. Corbineau","year":"2007","unstructured":"Corbineau, P., Kaliszyk, C.: Cooperative repositories for formal proofs. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM\/CALCULEMUS 2007. LNCS (LNAI), vol.\u00a04573, pp. 221\u2013234. Springer, Heidelberg (2007), http:\/\/www4.in.tum.de\/~kaliszyk\/docs\/cek_p3.pdf"},{"key":"37_CR5","volume-title":"Design Patterns \u2013 Elements of Reusable Object-Oriented Software","author":"E. Gamma","year":"1994","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns \u2013 Elements of Reusable Object-Oriented Software, 1st edn. Addison-Wesley, Reading (1994)","edition":"1"},{"key":"37_CR6","unstructured":"Geuvers, H., Mamane, L.: A document-oriented Coq plugin for TeXmacs. In: Libbrecht, P. (ed.) MathUI Workshop, MKM 2006 Conference, Wokingham, UK (2006), http:\/\/www.activemath.org\/~paul\/MathUI06\/"},{"key":"37_CR7","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C.: Web interfaces for proof assistants. In: Autexier, S., Benzm\u00fcller, C. (eds.) Proceedings of UITP 2006, Seattle. ENTCS, vol.\u00a0174(2), pp. 49\u201361 (2007), http:\/\/www4.in.tum.de\/~kaliszyk\/docs\/cek_p2.pdf","DOI":"10.1016\/j.entcs.2006.09.021"},{"key":"37_CR8","unstructured":"Kaliszyk, C.: Correctness and Availability. Building Computer Algebra on top of Proof Assistants and making Proof Assistants available over the Web. Ph.D. thesis, Radboud University Nijmegen (2009), http:\/\/www4.in.tum.de\/~kaliszyk\/docs\/ck_thesis_webdoc.pdf"},{"key":"37_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","DOI":"10.1007\/11826095","volume-title":"OMDoc \u2013 An Open Markup Format for Mathematical Documents [version 1.2]","author":"M. Kohlhase","year":"2006","unstructured":"Kohlhase, M.: OMDoc \u2013 An Open Markup Format for Mathematical Documents (version 1.2). LNCS (LNAI), vol.\u00a04180. Springer, Heidelberg (2006)"},{"key":"37_CR10","unstructured":"Matita Team: Matita interactive theorem prover. Web page, obtained from, http:\/\/matita.cs.unibo.it\/"},{"key":"37_CR11","unstructured":"Pierce, B.C., Casinghino, C., Greenberg, M.: Software foundations. Course notes (2010), http:\/\/www.cis.upenn.edu\/~bcpierce\/sf\/"},{"key":"37_CR12","unstructured":"Tankink, C., Geuvers, H., McKinna, J.: Narrating formal proof (work in progress). In: Submitted to UITP 2010 (2010), http:\/\/cs.ru.nl\/~carst\/files\/narration.pdf"},{"key":"37_CR13","volume-title":"PLMMS 2009","author":"M. Wenzel","year":"2009","unstructured":"Wenzel, M.: Parallel proof checking in Isabelle\/Isar. In: Reis, G.D., Th\u00e9ry, L. (eds.) PLMMS 2009. ACM, Munich (2009), http:\/\/www4.in.tum.de\/~wenzelm\/papers\/parallel-isabelle.pdf"}],"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-14128-7_37.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:47:53Z","timestamp":1606186073000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14128-7_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642141270","9783642141287"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14128-7_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}