{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:44:49Z","timestamp":1725489889010},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540749141"},{"type":"electronic","value":"9783540749158"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74915-8_26","type":"book-chapter","created":{"date-parts":[[2007,8,24]],"date-time":"2007-08-24T05:13:35Z","timestamp":1187932415000},"page":"328-342","source":"Crossref","is-referenced-by-count":7,"title":["Building Decision Procedures in the Calculus of Inductive Constructions"],"prefix":"10.1007","author":[{"given":"Fr\u00e9d\u00e9ric","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":"26_CR1","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":"26_CR2","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. Information and Computation\u00a076(2-3), 95\u2013120 (1988)","journal-title":"Information and Computation"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Types for Proofs and Programs","author":"G. Gonthier","year":"2006","unstructured":"Gonthier, G.: The four color theorem in coq. In: Filli\u00e2tre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol.\u00a03839, Springer, Heidelberg (2006)"},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/3-540-52335-9_47","volume-title":"COLOG-88","author":"T. Coquand","year":"1990","unstructured":"Coquand, T., Paulin-Mohring, C.: Inductively defined types. In: Martin-L\u00f6f, P., Mints, G. (eds.) COLOG-88. LNCS, vol.\u00a0417, pp. 50\u201366. Springer, Heidelberg (1990)"},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/BFb0055070","volume-title":"Automata, Languages and Programming","author":"E. Gim\u00e9nez","year":"1998","unstructured":"Gim\u00e9nez, E.: Structural recursive definitions in type theory. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443, pp. 397\u2013408. Springer, Heidelberg (1998)"},{"key":"26_CR6","unstructured":"Barras, B.: Auto-validation d\u2019un syst\u00e9me de preuves avec familles inductives. PhD thesis, Universit\u00e9 de Paris\u00a0VII (1999)"},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"Blanqui, F.: Definitions by rewriting in the calculus of constructions. Mathematical Structures in Computer Science, Journal version of LICS 2001.\u00a015(1), 37\u201392 (2005)","DOI":"10.1017\/S0960129504004426"},{"key":"26_CR8","unstructured":"Blanqui, F.: Inductive types in the calculus of algebraic constructions. Fundamenta Informaticae, Journal version of TLCA 2003.\u00a065(1-2), 61\u201386 (2005)"},{"issue":"2","key":"26_CR9","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1145\/322123.322137","volume":"26","author":"R.E. Shostak","year":"1979","unstructured":"Shostak, R.E.: An efficient decision procedure for arithmetic with function symbols. J. of the Association for Computing Machinery\u00a026(2), 351\u2013360 (1979)","journal-title":"J. of the Association for Computing Machinery"},{"key":"26_CR10","volume-title":"Proceedings of the Seventeenth Annual IEEE Symp. on Logic in Computer Science, LICS 2002","author":"N. Shankar","year":"2002","unstructured":"Shankar, N.: Little engines of proof. In: Plotkin, G. (ed.) Proceedings of the Seventeenth Annual IEEE Symp. on Logic in Computer Science, LICS 2002, IEEE Computer Society Press, Los Alamitos (2002) (Invited Talk)"},{"key":"26_CR11","unstructured":"Corbineau, P.: D\u00e9monstration automatique en Th\u00e9orie des Types. PhD thesis, University of Paris\u00a0IX (2005)"},{"key":"26_CR12","unstructured":"Stehr, M.: 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 (to appear, 2007)"},{"key":"26_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.\u00a03603, pp. 278\u2013293. Springer, Heidelberg (2005)"},{"key":"26_CR14","series-title":"Oxford Logic Guides","first-page":"83","volume-title":"Twenty-five years of constructive type theory","author":"M. Hofmann","year":"1998","unstructured":"Hofmann, M., Streicher, T.: The groupoid interpretation of type theory. In: Twenty-five years of constructive type theory. Oxford Logic Guides, vol.\u00a036, pp. 83\u2013111. Oxford University Press, Oxford (1998)"},{"key":"26_CR15","unstructured":"Blanqui, F., Jouannaud, J.P., Strub, P.Y.: A Calculus of Congruent Constructions, 2005 (unpublished draft)"},{"key":"26_CR16","series-title":"Handbook of logic in computer science","volume-title":"Lambda calculi with types","author":"H. Barendregt","year":"1992","unstructured":"Barendregt, H.: Lambda calculi with types. Handbook of logic in computer science, vol.\u00a02. Oxford University Press, Oxford (1992)"},{"key":"26_CR17","unstructured":"Werner, B.: Une Th\u00e9orie des Constructions Inductives. PhD thesis, University of Paris\u00a0VII (1994)"},{"key":"26_CR18","unstructured":"Blanqui, F.: Type Theory and Rewriting. PhD thesis, Universit\u00e9 de Paris\u00a0XI, Orsay, France (2001)"},{"key":"26_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055099","volume-title":"Automata, Languages and Programming","author":"G. Barthe","year":"1998","unstructured":"Barthe, G.: The relevance of proof irrelevance. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443, Springer, Heidelberg (1998)"},{"key":"26_CR20","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/S0747-7171(89)80022-7","volume":"8","author":"M. Schmidt-Schau\u00df","year":"1989","unstructured":"Schmidt-Schau\u00df, M.: Unification in a combination of arbitrary disjoint equational theories. J. Symbolic Computation, Special issue on Unification\u00a08, 51\u201399 (1989)","journal-title":"J. Symbolic Computation, Special issue on Unification"},{"key":"26_CR21","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Deduction - CADE-11","author":"F. Baader","year":"1992","unstructured":"Baader, F., Schulz, K.: Unification in the union of disjoint equational theories: Combining decision procedures. In: Kapur, D. (ed.) Automated Deduction - CADE-11. LNCS, vol.\u00a0607, Springer, Heidelberg (1992)"},{"key":"26_CR22","unstructured":"Strub, P.Y.: Type Theory and Decision Procedures. PhD thesis, \u00c9cole Polytechnique, Palaiseau, France (Work in progress)"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74915-8_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:45:49Z","timestamp":1619520349000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74915-8_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540749141","9783540749158"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74915-8_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}