{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,31]],"date-time":"2025-01-31T16:40:02Z","timestamp":1738341602619,"version":"3.35.0"},"publisher-location":"Boston, MA","reference-count":24,"publisher":"Springer US","isbn-type":[{"type":"print","value":"9780387096797"},{"type":"electronic","value":"9780387096803"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-0-387-09680-3_24","type":"book-chapter","created":{"date-parts":[[2008,7,21]],"date-time":"2008-07-21T11:37:14Z","timestamp":1216640234000},"page":"349-365","source":"Crossref","is-referenced-by-count":0,"title":["From Formal Proofs to Mathematical Proofs: A Safe, Incremental Way for Building in First-order Decision Procedures"],"prefix":"10.1007","author":[{"given":"Fr\u00e9deric","family":"Blanqui","sequence":"first","affiliation":[]},{"given":"Jean-Pierre","family":"Jouannaud","sequence":"additional","affiliation":[]},{"given":"Pierre-Yves","family":"Strub","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"H. Barendregt. Lambda calculi with types. In S. Abramski, D. Gabba, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume 2. Oxford University Press, 1992.","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"24_CR2","unstructured":"B. Barras. Auto-validation d\u2019un syst\u7b25 de preuves avec familles inductives. PhD thesis, University of Paris VII, 1999."},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"F. Blanqui. Definitions by rewriting in the calculus of constructions. Mathematical Structures in Computer Science, 15(1):37\u201392, 2005. Journal version of LICS\u201901.","DOI":"10.1017\/S0960129504004426"},{"issue":"1-2","key":"24_CR4","first-page":"61","volume":"65","author":"F. Blanqui","year":"2005","unstructured":"F. Blanqui. Inductive types in the calculus of algebraic constructions. Fundamenta Informaticae, 65(1-2):61\u201386, 2005. Journal version of TLCA\u201903.","journal-title":"Fundamenta Informaticae"},{"key":"24_CR5","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/3-540-48685-2_25","volume":"1631","author":"F. Blanqui","year":"1999","unstructured":"F. Blanqui, J.-P. Jouannaud, and M. Okada. The Calculus of Algebraic Constructions. In RTA, Lecture Notes in Computer Science 1631:301\u2013316. Springer-Verlag, 1999.","journal-title":"RTA, Lecture Notes in Computer Science"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"F. Blanqui, J. Jouannaud, and P. Strub. Building decision procedures in the calculus of inductive constructions. In Proceedings 16th CSL 2007. LNCS 4646, 2007.","DOI":"10.1007\/978-3-540-74915-8_26"},{"key":"24_CR7","unstructured":"F. Blanqui, J.-P. Jouannaud, and P.-Y. Strub. A Calculus of Congruent Constructions. Unpublished draft, 2005."},{"key":"24_CR8","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/S0304-3975(99)00206-6","volume":"236","author":"A. Bouhoula","year":"2000","unstructured":"A. Bouhoula, J.-P. Jouannaud, and J. Meseguer. Specification and proof in membership equational logic. Theoretical Comput. Sci., 236:35\u2013132, 2000.","journal-title":"Theoretical Comput. Sci."},{"key":"24_CR9","unstructured":"Coq-Development-Team. The Coq Proof Assistant Reference Manual - Version 8.0. INRIA, INRIA Rocquencourt, France, 2004. http:\/\/coq.inria.fr\/."},{"issue":"2-3","key":"24_CR10","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"T. Coquand and G. Huet. The Calculus of Constructions. Information and Computation, 76(2-3):95\u2013120, 1988.","journal-title":"Information and Computation"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"T. Coquand and C. Paulin-Mohring. Inductively defined types. Colog\u2019-88, International Conference on Computer Logic, volume 417 of LNCS, pages 50\u201366. Springer-Verlag, 1990.","DOI":"10.1007\/3-540-52335-9_47"},{"key":"24_CR12","unstructured":"P. Corbineau. D\u00e9monstration automatique en Th\u00e9orie des Types. PhD thesis, University of Paris IX, 2005."},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"K. Futatsugi, J. Goguen, J.-P. Jouannaud, and J. Meseguer. Principles of OBJ2. Proceedings of 12th ACM Conference on Principles of Programming Languages, 1985.","DOI":"10.1145\/318593.318610"},{"issue":"2","key":"24_CR14","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","volume":"1","author":"J.H. Geuvers","year":"1991","unstructured":"J. H. Geuvers and M. Nederhof. A modular proof of strong normalization for the calculus of constructions. J. of Functional programming, 1,2:155\u2013189, 1991.","journal-title":"J. of Functional programming"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"E. Gim\u00e9nez. Structural recursive definitions in type theory. In Proceedings of ICALP\u201998, volume 1443 of LNCS, pages 397\u2013408, July 1998.","DOI":"10.1007\/BFb0055070"},{"key":"24_CR16","unstructured":"G. Gonthier. The four color theorem in Coq. In TYPES 2004 International Workshop, 2004."},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"N. Oury. Extensionality in the calculus of constructions. In Proceedings 18th TPHOL, Oxford, UK. LNCS 3603, 2005.","DOI":"10.1007\/11541868_18"},{"key":"24_CR18","doi-asserted-by":"crossref","unstructured":"C. Paulin-Mohring. Inductive definitions in the system COQ. In Typed Lambda Calculi and Applications, pages 328\u2013345. Springer Verlag, 1993. LNCS 664.","DOI":"10.1007\/BFb0037116"},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"N. Shankar. Little engines of proof. In G. Plotkin, editor, Proceedings of the Seventeenth Annual IEEE Symp. on Logic in Computer Science. IEEE Computer Society Press, 2002.","DOI":"10.1109\/LICS.2002.1029812"},{"issue":"2","key":"24_CR20","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1145\/322123.322137","volume":"26","author":"R.E. Shostak","year":"1979","unstructured":"R. E. Shostak. An efficient decision procedure for arithmetic with function symbols. J. of the Association for Computing Machinery, 26(2):351\u2013360, 1979.","journal-title":"J. of the Association for Computing Machinery"},{"issue":"1-2","key":"24_CR21","doi-asserted-by":"crossref","first-page":"131","DOI":"10.3233\/FUN-2005-681-205","volume":"68","author":"M. Stehr","year":"2005","unstructured":"M. Stehr. The Open Calculus of Constructions: An equational type theory with dependent types for programming, specification, and interactive theorem proving (part I and II). Fundamenta Informaticae 68(1-2), p. 131-174, 2005.","journal-title":"Fundamenta Informaticae"},{"key":"24_CR22","unstructured":"T. Streicher. Investigations into intensional type theory, Habilitation, M\u00fcnich University, 1993."},{"key":"24_CR23","unstructured":"P.-Y. Strub. The Calculus of Congruent Inductive Constructions. PhD thesis, \u00c9cole Polytechnique, 2008."},{"key":"24_CR24","unstructured":"B. Werner. Une Th\u00e9orie des Constructions Inductives. PhD thesis, University Paris VII, 1994."}],"container-title":["IFIP International Federation for Information Processing","Fifth Ifip International Conference On Theoretical Computer Science \u2013 Tcs 2008"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-0-387-09680-3_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,31]],"date-time":"2025-01-31T03:13:53Z","timestamp":1738293233000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-0-387-09680-3_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9780387096797","9780387096803"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-0-387-09680-3_24","relation":{},"ISSN":["1571-5736"],"issn-type":[{"type":"print","value":"1571-5736"}],"subject":[]}}