{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,25]],"date-time":"2026-09-25T21:24:03Z","timestamp":1790371443666,"version":"4.1.0"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030510534","type":"print"},{"value":"9783030510541","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-51054-1_1","type":"book-chapter","created":{"date-parts":[[2020,6,29]],"date-time":"2020-06-29T19:02:39Z","timestamp":1593457359000},"page":"3-20","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Competing Inheritance Paths in\u00a0Dependent Type Theory: A Case Study in Functional Analysis"],"prefix":"10.1007","author":[{"given":"Reynald","family":"Affeldt","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cyril","family":"Cohen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marie","family":"Kerjean","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Assia","family":"Mahboubi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Damien","family":"Rouhling","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kazuhiko","family":"Sakaguchi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,6,24]]},"reference":[{"key":"1_CR1","unstructured":"Affeldt, R., Cohen, C., Kerjean, M., Mahboubi, A., Rouhling, D., Sakaguchi, K.: Formalizing functional analysis structures in dependent type theory (accompanying material). \nhttps:\/\/math-comp.github.io\/competing-inheritance-paths-in-dependent-type-theory\n\n (2020), contains the files packed_classes.v, packed_classes.v, type_classes.lean, and scalar_notations.v, and a stand-alone archive containing snapshots of the Mathematical Components [32] and Analysis [31] libraries"},{"key":"1_CR2","first-page":"43","volume":"11","author":"R Affeldt","year":"2018","unstructured":"Affeldt, R., Cohen, C., Rouhling, D.: Formalization techniques for asymptotic reasoning in classical analysis. J. Formaliz. Reason. 11, 43\u201376 (2018)","journal-title":"J. Formaliz. Reason."},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-03359-9_8","volume-title":"Theorem Proving in Higher Order Logics","author":"A Asperti","year":"2009","unstructured":"Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: Hints in unification. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 84\u201398. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-03359-9_8"},{"key":"1_CR4","unstructured":"Bauer, A., Gilbert, G., Haselwarter, P.G., Pretnar, M., Stone, C.A.: Design and implementation of the andromeda proof assistant. CoRR abs\/1802.06217 (2018). \nhttp:\/\/arxiv.org\/abs\/1802.06217"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Bauer, A., Gross, J., Lumsdaine, P.L., Shulman, M., Sozeau, M., Spitters, B.: The HoTT library: a formalization of homotopy type theory in Coq. In: 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017), Paris, France, 16\u201317 January 2017, pp. 164\u2013172. ACM (2017)","DOI":"10.1145\/3018610.3018615"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-540-71067-7_11","volume-title":"Theorem Proving in Higher Order Logics","author":"Y Bertot","year":"2008","unstructured":"Bertot, Y., Gonthier, G., Ould Biha, S., Pasca, I.: Canonical big operators. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 86\u2013101. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-71067-7_11"},{"issue":"1","key":"1_CR7","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/s11786-014-0181-1","volume":"9","author":"S Boldo","year":"2015","unstructured":"Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci. 9(1), 41\u201362 (2015)","journal-title":"Math. Comput. Sci."},{"key":"1_CR8","unstructured":"Bourbaki, N.: The architecture of mathematics. Am. Math. Mon. 57(4), 221\u2013232 (1950), \nhttp:\/\/www.jstor.org\/stable\/2305937"},{"key":"1_CR9","unstructured":"Bourbaki, N.: Th\u00e9orie des ensembles. \u00c9l\u00e9ments de math\u00e9matique. Springer (2006). Original Edition published by Hermann, Paris (1970)"},{"issue":"2","key":"1_CR10","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/0890-5401(91)90066-B","volume":"91","author":"NG de Bruijn","year":"1991","unstructured":"de Bruijn, N.G.: Telescopic mappings in typed lambda calculus. Inf. Comput. 91(2), 189\u2013204 (1991)","journal-title":"Inf. Comput."},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Buzzard, K., Commelin, J., Massot, P.: Formalising perfectoid spaces. In: 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), New Orleans, LA, USA, 20\u201321 January 2020, pp. 299\u2013312. ACM (2020)","DOI":"10.1145\/3372885.3373830"},{"key":"1_CR12","unstructured":"Cohen, C.: Formalized algebraic numbers: construction and first-order theory. (Formalisation des nombres alg\u00e9briques : construction et th\u00e9orie du premier ordre). Ph.D. thesis, Ecole Polytechnique X (2012). \nhttps:\/\/pastel.archives-ouvertes.fr\/pastel-00780446"},{"key":"1_CR13","doi-asserted-by":"publisher","unstructured":"Cohen, C., Mahboubi, A.: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Logic. Methods Comput. Sci. 8(1) (2012). \nhttps:\/\/doi.org\/10.2168\/LMCS-8(1:2)2012","DOI":"10.2168\/LMCS-8(1:2)2012"},{"key":"1_CR14","unstructured":"Cohen, C., Sakaguchi, K., Tassi, E.: Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi (2020). Accepted in the proceedings of FSCD 2020. \nhttps:\/\/hal.inria.fr\/hal-02478907"},{"key":"1_CR15","volume-title":"Implementing Mathematics with the NuPRL Proof Development System","author":"RL Constable","year":"1986","unstructured":"Constable, R.L., et al.: Implementing Mathematics with the NuPRL Proof Development System. Prentice-Hall, Upper Saddle River (1986)"},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/3-540-52335-9_47","volume-title":"COLOG-88","author":"T Coquand","year":"1990","unstructured":"Coquand, T., Paulin, C.: Inductively defined types. In: Martin-L\u00f6f, P., Mints, G. (eds.) COLOG 1988. LNCS, vol. 417, pp. 50\u201366. Springer, Heidelberg (1990). \nhttps:\/\/doi.org\/10.1007\/3-540-52335-9_47"},{"key":"1_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-03359-9_23","volume-title":"Theorem Proving in Higher Order Logics","author":"F Garillot","year":"2009","unstructured":"Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 327\u2013342. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-03359-9_23"},{"key":"1_CR18","doi-asserted-by":"publisher","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). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39634-2_14","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"1_CR19","unstructured":"Harrison, J.: The HOL Light System REFERENCE (2017). \nhttps:\/\/www.cl.cam.ac.uk\/~jrh13\/hol-light\/index.html"},{"key":"1_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-642-39634-2_5","volume-title":"Interactive Theorem Proving","author":"A Mahboubi","year":"2013","unstructured":"Mahboubi, A., Tassi, E.: Canonical structures for the working Coq user. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 19\u201334. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39634-2_5"},{"key":"1_CR21","unstructured":"Microsoft Reasearch: L$$\\exists \\forall $$N THEOREM PROVER (2020). \nhttps:\/\/leanprover.github.io"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction \u2013 CADE-25","author":"L de Moura","year":"2015","unstructured":"de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (System Description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378\u2013388. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-21401-6_26"},{"key":"1_CR23","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle HOL: A Proof Assistant for Higher-Order Logic. Springer (2019). \nhttps:\/\/isabelle.in.tum.de\/doc\/tutorial.pdf"},{"key":"1_CR24","unstructured":"Sa\u00efbi, A.: Outils G\u00e9n\u00e9riques de Mod\u00e9lisation et de D\u00e9monstration pour la Formalisation des Math\u00e9matiques en Th\u00e9orie des Types. Application \u00e0 la Th\u00e9orie des Cat\u00e9gories. (Formalization of Mathematics in Type Theory. Generic tools of Modelisation and Demonstration. Application to Category Theory). Ph.D. thesis, Pierre and Marie Curie University, Paris, France (1999)"},{"key":"1_CR25","series-title":"LNAI","first-page":"138","volume-title":"IJCAR 2020","author":"K Sakaguchi","year":"2020","unstructured":"Sakaguchi, K.: Validating mathematical structures. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNAI, vol. 12167, pp. 138\u2013157. Springer, Heidelberg (2020)"},{"key":"1_CR26","unstructured":"Selsam, D., Ullrich, S., de Moura, L.: Tabled typeclass resolution (2020). \nhttps:\/\/arxiv.org\/abs\/2001.04301"},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-540-71067-7_23","volume-title":"Theorem Proving in Higher Order Logics","author":"M Sozeau","year":"2008","unstructured":"Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 278\u2013293. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-71067-7_23"},{"issue":"4","key":"1_CR28","doi-asserted-by":"publisher","first-page":"795","DOI":"10.1017\/S0960129511000119","volume":"21","author":"B Spitters","year":"2011","unstructured":"Spitters, B., van der Weegen, E.: Type classes for mathematics in type theory. Math. Struct. Comput. Sci. 21(4), 795\u2013825 (2011)","journal-title":"Math. Struct. Comput. Sci."},{"key":"1_CR29","unstructured":"The Agda Team: The Agda User Manual (2020). \nhttps:\/\/agda.readthedocs.io\/en\/v2.6.0.1\n\n. Version 2.6.0.1"},{"key":"1_CR30","unstructured":"The Coq Development Team: The Coq Proof Assistant Reference Manual. Inria (2019). \nhttps:\/\/coq.inria.fr\n\n. Version 8.10.2"},{"key":"1_CR31","unstructured":"The Mathematical Components Analysis Team: The Mathematical Components Analysis library (2017). \nhttps:\/\/github.com\/math-comp\/analysis"},{"key":"1_CR32","unstructured":"The Mathematical Components Team: The Mathematical Components library (2007). \nhttps:\/\/github.com\/math-comp\/math-comp"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"The mathlib Community: The lean mathematical library. In: 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), New Orleans, LA, USA, 20\u201321 January 2020, pp. 367\u2013381. ACM (2020)","DOI":"10.1145\/3372885.3373824"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-51054-1_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,29]],"date-time":"2020-06-29T20:26:45Z","timestamp":1593462405000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-51054-1_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030510534","9783030510541"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-51054-1_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"24 June 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ijcar2020.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"150","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"31% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.03","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7.38","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11 system descriptions are also included. The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}