{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T06:04:37Z","timestamp":1726034677582},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030232498"},{"type":"electronic","value":"9783030232504"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-23250-4_17","type":"book-chapter","created":{"date-parts":[[2019,7,2]],"date-time":"2019-07-02T03:01:17Z","timestamp":1562036477000},"page":"243-257","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["A Plugin to Export Coq Libraries to XML"],"prefix":"10.1007","author":[{"given":"Claudio","family":"Sacerdoti Coen","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,7,3]]},"reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36469-2","volume-title":"Mathematical Knowledge Management","year":"2003","unstructured":"Asperti, A., Buchberger, B., Davenport, J.H. (eds.): MKM 2003. LNCS, vol. 2594. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36469-2"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/11617990_2","volume-title":"Types for Proofs and Programs","author":"A Asperti","year":"2006","unstructured":"Asperti, A., Guidi, F., Coen, C.S., Tassi, E., Zacchiroli, S.: A content based mathematical search engine: whelp. In: Filli\u00e2tre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol. 3839, pp. 17\u201332. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11617990_2"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-642-22438-6_7","volume-title":"Automated Deduction \u2013 CADE-23","author":"A Asperti","year":"2011","unstructured":"Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: The Matita interactive theorem prover. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 64\u201369. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_7"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-540-74464-1_2","volume-title":"Types for Proofs and Programs","author":"A Asperti","year":"2007","unstructured":"Asperti, A., Coen, C.S., Tassi, E., Zacchiroli, S.: Crafting a proof assistant. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 18\u201332. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74464-1_2"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/978-3-540-45155-6_2","volume-title":"Electronic Information and Communication in Mathematics","author":"A Asperti","year":"2003","unstructured":"Asperti, A., Wegner, B.: MOWGLI \u2013 an approach to machine-understandable representation of the mathematical information in digital documents. In: Bai, F., Wegner, B. (eds.) ICM 2002. LNCS, vol. 2730, pp. 14\u201323. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45155-6_2"},{"issue":"1\u20134","key":"17_CR6","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/s10817-018-9458-4","volume":"61","author":"L Czajka","year":"2018","unstructured":"Czajka, L., Kaliszyk, C.: Hammer for Coq: automation for dependent type theory. J. Autom. Reasoning 61(1\u20134), 423\u2013453 (2018). https:\/\/doi.org\/10.1007\/s10817-018-9458-4","journal-title":"J. Autom. Reasoning"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Condoluci, A., Kohlhase, M., M\u00fcller, D., Rabe, F., Sacerdoti Coen, C., Wenzel, M.: Relational data across mathematical libraries. In: Kaliszyk, C., et al. (eds.) CICM 2019. LNAI, vol. 11617, pp. 61\u201376 (2019)","DOI":"10.1007\/978-3-030-23250-4_5"},{"key":"17_CR8","unstructured":"Dowek, G., Thir\u00e9, F.: Logipedia: a multi-system encyclopedia of formal proofs. http:\/\/www.lsv.fr\/~dowek\/Publi\/logipedia.pdf"},{"key":"17_CR9","unstructured":"Arias, E.J.G.: SerAPI: Machine-friendly, data-centric serialization for Coq, October 2016. Working paper or preprint. https:\/\/hal-mines-paristech.archives-ouvertes.fr\/hal-01384408"},{"key":"17_CR10","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/3-540-36469-2_9","volume-title":"Lecture Notes in Computer Science","author":"Ferruccio Guidi","year":"2003","unstructured":"Guidi, F., Schena, I.: A query language for a metadata framework about mathematical resources. In: Asperti, et al. [ABD03], pp. 105\u2013118. https:\/\/doi.org\/10.1007\/3-540-36469-2_9"},{"key":"17_CR11","unstructured":"Irving, G., Szegedy, C., Alemi, A.A., E\u00e9n, N., Chollet, F., Urban, J.: DeepMath - deep sequence models for premise selection. In: Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems, Barcelona, Spain, 5\u201310 December 2016, pp. 2235\u20132243 (2016). http:\/\/papers.nips.cc\/paper\/6280-deepmath-deep-sequence-models-for-premise-selection"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/11856290_21","volume-title":"Artificial Intelligence and Symbolic Computation","author":"M Kohlhase","year":"2006","unstructured":"Kohlhase, M., Sucan, I.: A search engine for mathematical formulae. In: Calmet, J., Ida, T., Wang, D. (eds.) AISC 2006. LNCS, vol. 4120, pp. 241\u2013253. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11856290_21"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/3-540-48256-3_11","volume-title":"Theorem Proving in Higher Order Logics","author":"F Kamm\u00fcller","year":"1999","unstructured":"Kamm\u00fcller, F., Wenzel, M., Paulson, L.C.: Locales a sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Th\u00e9ry, L., Hirschowitz, A., Paulin, C. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 149\u2013165. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48256-3_11"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-319-62075-6_7","volume-title":"Intelligent Computer Mathematics","author":"D M\u00fcller","year":"2017","unstructured":"M\u00fcller, D., Gauthier, T., Kaliszyk, C., Kohlhase, M., Rabe, F.: Classification of alignments between concepts of formal mathematical systems. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM 2017. LNCS, vol. 10383, pp. 83\u201398. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-62075-6_7"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"M\u00fcller, D., Rabe, F., Sacerdoti Coen, C.: The Coq library as a theory graph. In: Kaliszyk, C., et al. (eds.) CICM 2019. LNAI, vol. 11617, pp. 171\u2013186 (2019)","DOI":"10.1007\/978-3-030-23250-4_12"},{"key":"17_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.ic.2013.06.001","volume":"230","author":"F Rabe","year":"2013","unstructured":"Rabe, F., Kohlhase, M.: A scalable module system. Inf. Comput. 230, 1\u201354 (2013). https:\/\/doi.org\/10.1016\/j.ic.2013.06.001","journal-title":"Inf. Comput."},{"key":"17_CR17","unstructured":"Sacerdoti Coen, C.: Project IST-2001-33562 MoWGLI. Technical report D2.a Exportation Module, Information Society Technologies (IST) Programme (2001). http:\/\/mowgli.cs.unibo.it\/misc\/deliverables\/transformation\/D2a_exportation_module\/report.pdf"},{"key":"17_CR18","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/3-540-36469-2_3","volume-title":"Lecture Notes in Computer Science","author":"Claudio Sacerdoti Coen","year":"2003","unstructured":"Sacerdoti Coen, C.: From proof-assistants to distributed libraries of mathematics: tips and pitfalls. In: Asperti, et al. [ABD03], pp. 30\u201344. https:\/\/doi.org\/10.1007\/3-540-36469-2_3"},{"key":"17_CR19","unstructured":"Sacerdoti Coen, C.: Mathematical knowledge management and interactive theorem proving. Ph.D. thesis, Technical report UBLCS 2004-5. University of Bologna (2004). http:\/\/www.cs.unibo.it\/~sacerdot\/tesidott\/thesis.ps.gz"},{"issue":"1\u20132","key":"17_CR20","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/s10817-009-9136-7","volume":"44","author":"C Sacerdoti Coen","year":"2010","unstructured":"Sacerdoti Coen, C.: Declarative representation of proof terms. J. Autom. Reasoning 44(1\u20132), 25\u201352 (2010). https:\/\/doi.org\/10.1007\/s10817-009-9136-7","journal-title":"J. Autom. Reasoning"},{"key":"17_CR21","doi-asserted-by":"publisher","unstructured":"The Coq Development Team: The Coq Proof Assistant, version 8.9.0, January 2019. https:\/\/doi.org\/10.5281\/zenodo.2554024","DOI":"10.5281\/zenodo.2554024"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-23250-4_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,12,1]],"date-time":"2019-12-01T20:26:23Z","timestamp":1575231983000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-23250-4_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030232498","9783030232504"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-23250-4_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"3 July 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2019\/cicm.php?event=&menu=general","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}