{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T10:48:25Z","timestamp":1776509305535,"version":"3.51.2"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032070203","type":"print"},{"value":"9783032070210","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-07021-0_15","type":"book-chapter","created":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T13:41:00Z","timestamp":1759844460000},"page":"258-275","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Indexing and Retrieval in a Heterogeneous Formal Library"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4360-6016","authenticated-orcid":false,"given":"Claudio","family":"Sacerdoti Coen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4921-1522","authenticated-orcid":false,"given":"Abdelghani","family":"Alidra","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"F.\u00a0Thir\u00e9, Interoperability between proof systems using the logical framework Dedukti. (Interop\u00e9rabilit\u00e9 entre syst\u00e8mes de preuve en utilisant le cadre logique Dedukti). PhD thesis, \u00c9cole normale sup\u00e9rieure Paris-Saclay, Cachan, France, 2020."},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"F.\u00a0Guidi and C.\u00a0S. Coen, \u201cA survey on retrieval of mathematical knowledge,\u201d Math. Comput. Sci., vol.\u00a010, no.\u00a04, pp.\u00a0409\u2013427, 2016.","DOI":"10.1007\/s11786-016-0274-0"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"P.\u00a0Dadure, P.\u00a0Pakray, and S.\u00a0Bandyopadhyay, \u201cMathematical information retrieval: A review,\u201d ACM Comput. Surv., vol.\u00a057, no.\u00a03, pp.\u00a061:1\u201361:34, 2025.","DOI":"10.1145\/3699953"},{"key":"15_CR4","unstructured":"R.\u00a0Harper, F.\u00a0Honsell, and G.\u00a0D. Plotkin, \u201cA framework for defining logics,\u201d in Proceedings of the Symposium on Logic in Computer Science (LICS \u201987), Ithaca, New York, USA, June 22-25, 1987, pp.\u00a0194\u2013204, IEEE Computer Society, 1987."},{"key":"15_CR5","unstructured":"G.\u00a0Dowek, \u201cDeduction modulo theory,\u201d CoRR, vol.\u00a0abs\/1501.06523, 2015."},{"key":"15_CR6","unstructured":"C.\u00a0Prodescu and M.\u00a0Kohlhase, \u201cMathwebsearch 0.5 an open formula search engine,\u201d in Report of the symposium \"Lernen, Wissen, Adaptivit\u00e4t 2011\" of the GI special interest groups KDML, IR and WM, LWA 2011, Magdeburg, 28.-30.September 2011 (M.\u00a0Spiliopoulou, A.\u00a0N\u00fcrnberger, and R.\u00a0Schult, eds.), pp.\u00a0257\u2013264, Fakult\u00e4t f\u00fcr Informatik, Otto-von-Guericke-Universit\u00e4t Magdeburg, 2011."},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"A.\u00a0Church, \u201cA formulation of the simple theory of types,\u201d The journal of symbolic logic, vol.\u00a05, no.\u00a02, pp.\u00a056\u201368, 1940.","DOI":"10.2307\/2266170"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"J.\u00a0Hurd, \u201cThe opentheory standard theory library,\u201d in NASA Formal Methods Symposium, pp.\u00a0177\u2013191, Springer, 2011.","DOI":"10.1007\/978-3-642-20398-5_14"},{"key":"15_CR9","unstructured":"T.\u00a0Coquand and G.\u00a0Huet, The calculus of constructions. PhD thesis, INRIA, 1986."},{"key":"15_CR10","unstructured":"H.\u00a0P. Barendregt, Lambda calculi with types, p.\u00a0117\u2013309. USA: Oxford University Press, Inc., 1993."},{"key":"15_CR11","unstructured":"H.\u00a0B. Curry, J.\u00a0R. Hindley, and J.\u00a0P. Seldin, To HB Curry: essays on combinatory logic, lambda calculus, and formalism. Academic Press, 1980."},{"key":"15_CR12","unstructured":"A.\u00a0Assaf, G.\u00a0Burel, R.\u00a0Cauderlier, D.\u00a0Delahaye, G.\u00a0Dowek, C.\u00a0Dubois, F.\u00a0Gilbert, P.\u00a0Halmagrand, O.\u00a0Hermant, and R.\u00a0Saillard, \u201cDedukti: a logical framework based on the $$\\lambda $$$$\\varPi $$-calculus modulo theory,\u201d CoRR, vol.\u00a0abs\/2311.07185, 2023."},{"key":"15_CR13","unstructured":"ROCQ Prover, \u201cRocq prover,\u201d 2023. Accessed: 2025-07-06."},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"L.\u00a0de\u00a0Moura, \u201cSoonho kong, jeremy avigad, floris van doorn, and jakob von raumer,\u201d The Lean Theorem Prover (system description), pp.\u00a0378\u2013388, 2014.","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"D.\u00a0M\u00fcller, T.\u00a0Gauthier, C.\u00a0Kaliszyk, M.\u00a0Kohlhase, and F.\u00a0Rabe, \u201cClassification of alignments between concepts of formal mathematical systems,\u201d in Intelligent Computer Mathematics - 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings, vol.\u00a010383 of Lecture Notes in Computer Science, pp.\u00a083\u201398, Springer, 2017.","DOI":"10.1007\/978-3-319-62075-6_7"},{"key":"15_CR16","unstructured":"L.\u00a0Horowitz and V.\u00a0de\u00a0Paiva, \u201cMathgloss: Building mathematical glossaries from text,\u201d CoRR, vol.\u00a0abs\/2311.12649, 2023."},{"key":"15_CR17","unstructured":"G.\u00a0Hondet and F.\u00a0Blanqui, \u201cThe new rewriting engine of dedukti (system description),\u201d in 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference) (Z.\u00a0M. Ariola, ed.), vol.\u00a0167 of LIPIcs, pp.\u00a035:1\u201335:16, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2020."},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"M.\u00a0F\u00e4rber, \u201cSafe, fast, concurrent proof checking for the lambda-pi calculus modulo rewriting,\u201d in Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2022, (New York, NY, USA), p.\u00a0225\u2013238, 2022.","DOI":"10.1145\/3497775.3503683"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"A.\u00a0Asperti, F.\u00a0Guidi, C.\u00a0S. Coen, E.\u00a0Tassi, and S.\u00a0Zacchiroli, \u201cA content based mathematical search engine: Whelp,\u201d in Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers, vol.\u00a03839 of Lecture Notes in Computer Science, pp.\u00a017\u201332, Springer, 2004.","DOI":"10.1007\/11617990_2"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"J.\u00a0Harrison, \u201cHol light: A tutorial introduction,\u201d in International Conference on Formal Methods in Computer-Aided Design, pp.\u00a0265\u2013269, Springer, 1996.","DOI":"10.1007\/BFb0031814"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"F.\u00a0Blanqui, \u201cTranslating HOL-Light proofs to Coq,\u201d in LPAR 2024: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, Port Louis, Mauritius, May 26-31, 2024, vol.\u00a0100 of EPiC Series in Computing, pp.\u00a01\u201318, EasyChair, 2024.","DOI":"10.29007\/6k4x"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-07021-0_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T10:22:22Z","timestamp":1776507742000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-07021-0_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032070203","9783032070210"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-07021-0_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"8 October 2025","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":"Brasilia","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazil","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 October 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2025\/cicm.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}