{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,17]],"date-time":"2026-04-17T11:03:17Z","timestamp":1776423797688,"version":"3.51.2"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319214009","type":"print"},{"value":"9783319214016","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21401-6_26","type":"book-chapter","created":{"date-parts":[[2015,7,24]],"date-time":"2015-07-24T10:13:46Z","timestamp":1437732826000},"page":"378-388","source":"Crossref","is-referenced-by-count":262,"title":["The Lean Theorem Prover (System Description)"],"prefix":"10.1007","author":[{"given":"Leonardo","family":"de Moura","sequence":"first","affiliation":[]},{"given":"Soonho","family":"Kong","sequence":"additional","affiliation":[]},{"given":"Jeremy","family":"Avigad","sequence":"additional","affiliation":[]},{"given":"Floris","family":"van Doorn","sequence":"additional","affiliation":[]},{"given":"Jakob","family":"von Raumer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,25]]},"reference":[{"key":"26_CR1","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)"},{"key":"26_CR2","unstructured":"Avigad, J., de Moura, L., Kong,S.: Theorem Proving in Lean (2015). http:\/\/leanprover.github.io\/tutorial\/tutorial.pdf"},{"key":"26_CR3","unstructured":"Barras, B., Boutin, S., Cornes, C., Courant, J., Filliatre, J.-C., Gimenez, E., Herbelin, H., Huet, G., Munoz, C., Murthy, C. et al.: The Coq proof assistant reference manual: Version 6.1 (1997)"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"Cockx, J., Devriese, D., Piessens, F.: Pattern matching without K. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, pp. 257\u2013268. ACM (2014)","DOI":"10.1145\/2692915.2628139"},{"issue":"2\u20133","key":"26_CR5","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.: The calculus of constructions. Inf. Comput. 76(2\u20133), 95\u2013120 (1988)","journal-title":"Inf. Comput."},{"key":"26_CR6","unstructured":"Coquand, T., Paulin, C.: Inductively defined types. In: COLOG-88 (Tallinn, 1988), pp. 50\u201366. Springer, Berlin (1990)"},{"key":"26_CR7","unstructured":"de Moura, L., Avigad, J., Kong, S., Roux, C.: Elaboration in dependent type theory. Preprint (arXiv)"},{"key":"26_CR8","unstructured":"Delahaye, D., Woltzenlogel Paleo, B. (eds.): All about proofs, proofs for all. Mathematical Logic and Foundations, vol. 55 (2015)"},{"issue":"4","key":"26_CR9","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/BF01211308","volume":"6","author":"P Dybjer","year":"1994","unstructured":"Dybjer, P.: Inductive families. Formal Aspects Comput. 6(4), 440\u2013465 (1994)","journal-title":"Formal Aspects Comput."},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/11780274_27","volume-title":"Algebra, Meaning, and Computation","author":"HH Goguen","year":"2006","unstructured":"Goguen, H.H., McBride, C., McKinna, J.: Eliminating dependent pattern matching. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Algebra, Meaning, and Computation. LNCS, vol. 4060, pp. 521\u2013540. Springer, Heidelberg (2006)"},{"key":"26_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-03359-9_4","volume-title":"Theorem Proving in Higher Order Logics","author":"J Harrison","year":"2009","unstructured":"Harrison, J.: HOL light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60\u201366. Springer, Heidelberg (2009)"},{"key":"26_CR12","unstructured":"Martin-L\u00f6f, P.: Intuitionistic type theory. Bibliopolis (1984)"},{"key":"26_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/11617990_12","volume-title":"Types for Proofs and Programs","author":"C McBride","year":"2006","unstructured":"McBride, C., Goguen, H.H., McKinna, J.: A few constructions on constructors. In: Filli\u00e2tre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol. 3839, pp. 186\u2013200. Springer, Heidelberg (2006)"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"McBride, C., McKinna, J.: Functional pearl: I am not a number-I am a free variable. In: Proceedings of the 2004 ACM SIGPLAN Workshop on Haskell, Haskell 2004, pp. 1\u20139. ACM, New York (2004)","DOI":"10.1145\/1017472.1017477"},{"key":"26_CR15","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139021326","volume-title":"Programming with Higher-Order Logic","author":"D Miller","year":"2012","unstructured":"Miller, D., Nadathur, G.: Programming with Higher-Order Logic. Cambridge University Press, Cambridge (2012)"},{"key":"26_CR16","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - CADE-11","author":"T Nipkow","year":"1992","unstructured":"Nipkow, T., Paulson, L.C.: Isabelle-91. In: Kapur, Deepak (ed.) CADE 1992. LNCS, vol. 607. Springer, Heidelberg (1992)"},{"key":"26_CR17","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: a proof assistant for higher-order logic, vol. 2283. Springer Science and Business Media (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"26_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-642-04652-0_5","volume-title":"Advanced Functional Programming","author":"U Norell","year":"2009","unstructured":"Norell, U.: Dependently typed programming in Agda. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832, pp. 230\u2013266. Springer, Heidelberg (2009)"},{"key":"26_CR19","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J., Shankar, N.: PVS: a prototype verification system. In: Kapur, Deepak (ed.) CADE 1992. LNCS, vol. 607. Springer, Heidelberg (1992)"},{"key":"26_CR20","unstructured":"Rudnicki, P.: An overview of the Mizar project. In: Proceedings of the 1992 Workshop on Types for Proofs and Programs, pp. 311\u2013330 (1992)"},{"key":"26_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0105417","volume-title":"Theorem Proving in Higher Order Logics","author":"K Slind","year":"1996","unstructured":"Slind, K.: Function definition in higher-order logic. In: von Wright, Joakim, Harrison, J., Grundy, John (eds.) TPHOLs 1996. LNCS, vol. 1125. Springer, Heidelberg (1996)"},{"key":"26_CR22","unstructured":"Streicher, T.: Investigations into intensional type theory. Ph.D. thesis, LMU (1993)"},{"key":"26_CR23","unstructured":"The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study (2013)"},{"key":"26_CR24","unstructured":"Wenzel, M.M.: Isabelle\/Isar - a versatile environment for human-readable formal proof documents. Technical report ( 2002)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-25"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21401-6_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,28]],"date-time":"2019-08-28T17:36:19Z","timestamp":1567013779000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21401-6_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214009","9783319214016"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}