{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:06:24Z","timestamp":1784844384191,"version":"3.55.0"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032111753","type":"print"},{"value":"9783032111760","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,23]],"date-time":"2025-11-23T00:00:00Z","timestamp":1763856000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,23]],"date-time":"2025-11-23T00:00:00Z","timestamp":1763856000000},"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-11176-0_13","type":"book-chapter","created":{"date-parts":[[2025,11,22]],"date-time":"2025-11-22T20:11:30Z","timestamp":1763842290000},"page":"202-219","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Lean4Less: Eliminating Definitional Equalities from\u00a0Lean via\u00a0an\u00a0Extensional-to-Intensional Translation"],"prefix":"10.1007","author":[{"given":"Rishikesh","family":"Vaishnav","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,11,23]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","unstructured":"Abel, A., Coquand, T.: Failure of normalization in impredicative type theory with proof-irrelevant propositional equality. Log. Methods Comput. Sci. 16(2), 14 (2020). https:\/\/doi.org\/10.23638\/LMCS-16(2:14)2020","DOI":"10.23638\/LMCS-16(2:14)2020"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/10721959_12","volume-title":"Automated Deduction - CADE-17","author":"SF Allen","year":"2000","unstructured":"Allen, S.F., Constable, R.L., Eaton, R., Kreitz, C., Lorigo, L.: The Nuprl open logical environment. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol. 1831, pp. 170\u2013176. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10721959_12"},{"key":"13_CR3","doi-asserted-by":"publisher","unstructured":"Bauer, A., Gilbert, G., Haselwarter, P.G., Pretnar, M., Stone, C.A.: Design and implementation of the andromeda proof assistant. In: Ghilezan, S., Geuvers, H., Ivetic, J. (eds.) 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a097, pp. 5:1\u20135:31. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2018). https:\/\/doi.org\/10.4230\/LIPIcs.TYPES.2016.5","DOI":"10.4230\/LIPIcs.TYPES.2016.5"},{"key":"13_CR4","doi-asserted-by":"publisher","unstructured":"Blanqui, F., Dowek, G., Grienenberger, E., Hondet, G., Thir\u00e9, F.: A modular construction of type theories. Log. Methods Comput. Sci. 19(1), 12 (2023). https:\/\/doi.org\/10.46298\/lmcs-19(1:12)2023","DOI":"10.46298\/lmcs-19(1:12)2023"},{"key":"13_CR5","unstructured":"Carneiro, M.: The Type Theory of Lean. Master\u2019s thesis (2019). https:\/\/github.com\/digama0\/lean-type-theory\/releases\/tag\/v1.0"},{"key":"13_CR6","unstructured":"Carneiro, M.: Lean4lean: towards a formalized metatheory for the lean theorem prover (2024). https:\/\/arxiv.org\/abs\/2403.14064"},{"key":"13_CR7","doi-asserted-by":"publisher","unstructured":"Forster, Y., Sozeau, M., Tabareau, N.: Verified extraction from Coq to OCaml (2024). https:\/\/doi.org\/10.1145\/3656379","DOI":"10.1145\/3656379"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Hofmann, M.: Conservativity of equality reflection over intensional type theory. In: Selected Papers from the International Workshop on Types for Proofs and Programs, TYPES 1995, pp. 153\u2013164. Springer, Heidelberg (1995)","DOI":"10.1007\/3-540-61780-9_68"},{"key":"13_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0963-1","volume-title":"Extensional Constructs in Intensional Type Theory","author":"M Hofmann","year":"1997","unstructured":"Hofmann, M., Rijsbergen, C.J.: Extensional Constructs in Intensional Type Theory. Springer, Heidelberg (1997)"},{"key":"13_CR10","doi-asserted-by":"publisher","unstructured":"Hondet, G., Blanqui, F.: Encoding of predicate subtyping with proof irrelevance in the $$\\lambda \\Pi $$-calculus modulo theory. In: de\u2019Liguoro, U., Berardi, S., Altenkirch, T. (eds.) 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0188, pp. 6:1\u20136:18. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2021). https:\/\/doi.org\/10.4230\/LIPIcs.TYPES.2020.6","DOI":"10.4230\/LIPIcs.TYPES.2020.6"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1007\/978-3-030-79876-5_37","volume-title":"Automated Deduction \u2013 CADE 28","author":"L Moura","year":"2021","unstructured":"Moura, L., Ullrich, S.: The lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 625\u2013635. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/11541868_18","volume-title":"Theorem Proving in Higher Order Logics","author":"N Oury","year":"2005","unstructured":"Oury, N.: Extensionality in the calculus of constructions. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 278\u2013293. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11541868_18"},{"key":"13_CR13","unstructured":"Paulin-Mohring, C.: Introduction to the calculus of inductive constructions. In: Paleo, B.W., Delahaye, D. (eds.) All about Proofs, Proofs for All, Studies in Logic (Mathematical logic and foundations), vol.\u00a055. College Publications (2015). https:\/\/inria.hal.science\/hal-01094195"},{"key":"13_CR14","unstructured":"Rocq Community: The Rocq theorem prover. https:\/\/rocq-prover.org\/"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Sozeau, M., Boulier, S., Forster, Y., Tabareau, N., Winterhalter, T.: Coq coq correct! Verification of type checking and erasure for coq, in coq. Proc. ACM Program. Lang. 4(POPL) (2019). https:\/\/doi.org\/10.1145\/3371076","DOI":"10.1145\/3371076"},{"issue":"1","key":"13_CR16","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/2914770.2837655","volume":"51","author":"N Swamy","year":"2016","unstructured":"Swamy, N., et al.: Dependent types and multi-monadic effects in F*. SIGPLAN Not. 51(1), 256\u2013270 (2016). https:\/\/doi.org\/10.1145\/2914770.2837655","journal-title":"SIGPLAN Not."},{"key":"13_CR17","unstructured":"The mathlib community: mathlib4 (Github). https:\/\/github.com\/leanprover-community\/mathlib4"},{"key":"13_CR18","doi-asserted-by":"publisher","unstructured":"The mathlib community: The lean mathematical library. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pp. 367\u2013381. Association for Computing Machinery, New York (2020). https:\/\/doi.org\/10.1145\/3372885.3373824","DOI":"10.1145\/3372885.3373824"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Winterhalter, T., Sozeau, M., Tabareau, N.: Eliminating reflection from type theory. In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (2019). https:\/\/api.semanticscholar.org\/CorpusID:57379755","DOI":"10.1145\/3293880.3294095"},{"key":"13_CR20","unstructured":"Winterhalter, T., Tabareau, N.: ett-to-itt (Github). https:\/\/github.com\/TheoWinterhalter\/ett-to-itt"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2025"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-11176-0_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T11:09:54Z","timestamp":1770721794000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-11176-0_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,23]]},"ISBN":["9783032111753","9783032111760"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-11176-0_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,23]]},"assertion":[{"value":"23 November 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The author claims no competing interests.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"ICTAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Theoretical Aspects of Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Marrakesh","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Morocco","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":"24 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ictac2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ictac2025.digital-hub.sh\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}