{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:10Z","timestamp":1774837810446,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540314288","type":"print"},{"value":"9783540314295","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11617990_2","type":"book-chapter","created":{"date-parts":[[2006,1,19]],"date-time":"2006-01-19T11:39:40Z","timestamp":1137670780000},"page":"17-32","source":"Crossref","is-referenced-by-count":24,"title":["A Content Based Mathematical Search Engine: Whelp"],"prefix":"10.1007","author":[{"given":"Andrea","family":"Asperti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ferruccio","family":"Guidi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claudio Sacerdoti","family":"Coen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enrico","family":"Tassi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefano","family":"Zacchiroli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Asperti, A., Guidi, F., Padovani, L., Sacerdoti Coen, C., Schena, I.: The Science of Equality: some statistical considerations on the Coq library. In: Mathematical Knowledge Management Symposium, Heriot-Watt University, Edinburgh, Scotland, November 25-29 (2003)","DOI":"10.1007\/3-540-36469-2"},{"issue":"1","key":"2_CR2","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1023\/A:1022907629104","volume":"38","author":"A. Asperti","year":"2003","unstructured":"Asperti, A., Guidi, F., Padovani, L., Sacerdoti Coen, C., Schena, I.: Mathematical Knowledge Management in HELM. Annals of Mathematics and Artificial Intelligence\u00a038(1), 27\u201346 (2003)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-540-27818-4_2","volume-title":"Mathematical Knowledge Management","author":"A. Asperti","year":"2004","unstructured":"Asperti, A., Selmi, M.: Efficient Retrieval of Mathematical Statements. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol.\u00a03119, pp. 17\u201331. Springer, Heidelberg (2004)"},{"key":"2_CR4","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.: An Approach to Machine-Understandable Representation of the Mathematical Information in Digital Documents. In: Bai, F., Wegner, B. (eds.) ICM 2002. LNCS, vol.\u00a02730, pp. 14\u201323. Springer, Heidelberg (2003)"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/3-540-36469-2_10","volume-title":"Mathematical Knowledge Management","author":"G. Bancerek","year":"2003","unstructured":"Bancerek, G., Rudnicki, P.: Information Retrieval in MML. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol.\u00a02594, pp. 119\u2013132. Springer, Heidelberg (2003)"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-540-27818-4_4","volume-title":"Mathematical Knowledge Management","author":"G. Bancerek","year":"2004","unstructured":"Bancerek, G., Urban, J.: Integrated Semantic Browsing of the Mizar Mathematical Repository. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol.\u00a03119, pp. 44\u201357. Springer, Heidelberg (2004)"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-540-27818-4_5","volume-title":"Mathematical Knowledge Management","author":"P. Cairns","year":"2004","unstructured":"Cairns, P.: Informalising Formal Mathematics: Searching the Mizar Library with Latent Semantics. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol.\u00a03119, pp. 58\u201372. Springer, Heidelberg (2004)"},{"key":"2_CR8","unstructured":"The Coq proof-assistant, \n                  \n                    http:\/\/coq.inria.fr"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-540-27818-4_7","volume-title":"Mathematical Knowledge Management","author":"L. Cruz-Filipe","year":"2004","unstructured":"Cruz-Filipe, L., Geuvers, H., Wiedijk, F.: C-CoRN, the Constructive Coq Repository at Nijmegen. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol.\u00a03119, pp. 88\u2013103. Springer, Heidelberg (2004)"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/3-540-44557-9_8","volume-title":"Types for Proofs and Programs","author":"D. Delahaye","year":"2000","unstructured":"Delahaye, D., Di Cosmo, R.: Information Retrieval in a Coq Proof Library using Type Isomorphisms. In: Coquand, T., Nordstr\u00f6m, B., Dybjer, P., Smith, J. (eds.) TYPES 1999. LNCS, vol.\u00a01956, pp. 131\u2013147. Springer, Heidelberg (2000)"},{"key":"2_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2572-0","volume-title":"Isomorphisms of Types: from Lambda Calculus to Information Retrieval and Language Design","author":"R. Cosmo Di","year":"1995","unstructured":"Di Cosmo, R.: Isomorphisms of Types: from Lambda Calculus to Information Retrieval and Language Design. Birkhauser, Basel (1995) IBSN-0-8176-3763-X"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Nieuwehuis, R., Nivela, P.: Fast Term Indexing with Coded Context Trees. Journal of Automated Reasoning (to appear)","DOI":"10.1023\/B:JARS.0000029963.64213.ac"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/3-540-59200-8_52","volume-title":"Rewriting Techniques and Applications","author":"P. Graf","year":"1995","unstructured":"Graf, P.: Substitution Tree Indexing. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol.\u00a0914, pp. 117\u2013131. Springer, Heidelberg (1995)"},{"key":"2_CR14","unstructured":"Guidi, F., Sacerdoti Coen, C.: Querying Distributed Digital Libraries of Mathematics. In: Proceedings of Calculemus 2003, 11th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Aracne Editrice (2003)"},{"key":"2_CR15","unstructured":"McBride, C.: Dependently Typed Functional Programs and their Proofs. Ph.D. thesis, University of Edinburgh (1999)"},{"issue":"2","key":"2_CR16","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF00245458","volume":"9","author":"W. McCune","year":"1992","unstructured":"McCune, W.: Experiments with discrimination tree indexing and path indexing for term retrieval. Journal of Automated Reasoning\u00a09(2), 147\u2013167 (1992)","journal-title":"Journal of Automated Reasoning"},{"key":"2_CR17","unstructured":"Munoz, C.: A Calculus of Substitutions for Incomplete-Proof Representation in Type Theory. Ph.D. thesis, INRIA (1997)"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/3-540-36469-2_3","volume-title":"Mathematical Knowledge Management","author":"C. Sacerdoti Coen","year":"2003","unstructured":"Sacerdoti Coen, C.: From Proof-Assistans to Distributed Libraries of Mathematics: Tips and Pitfalls. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol.\u00a02594, pp. 30\u201344. Springer, Heidelberg (2003)"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-540-27818-4_25","volume-title":"Mathematical Knowledge Management","author":"C. Sacerdoti Coen","year":"2004","unstructured":"Sacerdoti Coen, C., Zacchiroli, S.: Efficient Ambiguous Parsing of Mathematical Formulae. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol.\u00a03119, pp. 347\u2013362. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11617990_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:12:00Z","timestamp":1619507520000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11617990_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540314288","9783540314295"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/11617990_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}