{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T18:19:21Z","timestamp":1781893161841,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540371878","type":"print"},{"value":"9783540371885","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814771_50","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T11:44:21Z","timestamp":1160048661000},"page":"619-631","source":"Crossref","is-referenced-by-count":3,"title":["Consistency and Completeness of Rewriting in the Calculus of Constructions"],"prefix":"10.1007","author":[{"given":"Daria","family":"Walukiewicz-Chrz\u0105szcz","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jacek","family":"Chrz\u0105szcz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"6","key":"50_CR1","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1017\/S095679689700289X","volume":"7","author":"F. Barbanera","year":"1997","unstructured":"Barbanera, F., Fern\u00e1ndez, M., Geuvers, H.: Modularity of strong normalization in the algebraic-\u03bb-cube. Journal of Functional Programming\u00a07(6), 613\u2013660 (1997)","journal-title":"Journal of Functional Programming"},{"key":"50_CR2","first-page":"117","volume-title":"Handbook of Logic in Computer Science, ch. 2","author":"H. Barendregt","year":"1992","unstructured":"Barendregt, H.: Lambda calculi with types. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, ch. 2, pp. 117\u2013309. Oxford University Press, Oxford (1992)"},{"key":"50_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/11538363_12","volume-title":"Computer Science Logic","author":"B. Barras","year":"2005","unstructured":"Barras, B., Gr\u00e9goire, B.: On the role of type decorations in the calculus of inductive constructions. In: Ong, L. (ed.) CSL 2005. LNCS, vol.\u00a03634, pp. 151\u2013166. Springer, Heidelberg (2005)"},{"issue":"1","key":"50_CR4","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1017\/S0960129504004426","volume":"15","author":"F. Blanqui","year":"2005","unstructured":"Blanqui, F.: Definitions by rewriting in the Calculus of Constructions. Mathematical Structures in Computer Science\u00a015(1), 37\u201392 (2005)","journal-title":"Mathematical Structures in Computer Science"},{"key":"50_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/3-540-48685-2_25","volume-title":"Rewriting Techniques and Applications","author":"F. Blanqui","year":"1999","unstructured":"Blanqui, F., Jouannaud, J.-P., Okada, M.: The Calculus of Algebraic Constructions. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol.\u00a01631, pp. 301\u2013316. Springer, Heidelberg (1999)"},{"key":"50_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-540-24849-1_8","volume-title":"Types for Proofs and Programs","author":"E. Brady","year":"2004","unstructured":"Brady, E., McBride, C., McKinna, J.: Inductive families need not store their indices. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, pp. 115\u2013129. Springer, Heidelberg (2004)"},{"key":"50_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-540-24849-1_9","volume-title":"Types for Proofs and Programs","author":"J. Chrzaszcz","year":"2004","unstructured":"Chrz\u0105szcz, J.: Modules in Coq are and will be correct. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, pp. 130\u2013146. Springer, Heidelberg (2004)"},{"key":"50_CR8","unstructured":"Chrz\u0105szcz, J.: Modules in Type Theory with Generative Definitions. PhD thesis, Warsaw Univerity and University of Paris-Sud (January 2004)"},{"key":"50_CR9","unstructured":"The Coq proof assistant, http:\/\/coq.inria.fr\/"},{"key":"50_CR10","unstructured":"Coquand, T.: Pattern matching with dependent types. In: Proceedings of the Workshop on Types for Proofs and Programs, B\u00e5stad, Sweden, pp. 71\u201383 (1992)"},{"key":"50_CR11","unstructured":"Cornes, C.: Conception d\u2019un langage de haut niveau de r\u00e9presentation de preuves. PhD thesis, Universit\u00e9 Paris VII (1997)"},{"key":"50_CR12","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/BF00260922","volume":"10","author":"J.V. Guttag","year":"1978","unstructured":"Guttag, J.V., Horning, J.J.: The algebraic specification of abstract data types. Acta Informatica\u00a010, 27\u201352 (1978)","journal-title":"Acta Informatica"},{"key":"50_CR13","series-title":"Lecture Notes in Computer Science","first-page":"348","volume-title":"EUROCAL \u201985. European Conference on Computer Algebra. Linz, Austria, April 1-3, 1985. Proceedings","author":"E. Kounalis","year":"1985","unstructured":"Kounalis, E.: Completeness in data type specifications. In: Caviness, B.F. (ed.) ISSAC 1985 and EUROCAL 1985. LNCS, vol.\u00a0204, pp. 348\u2013362. Springer, Heidelberg (1985)"},{"key":"50_CR14","unstructured":"McBride, C.: Dependently Typed Functional Programs and Their Proofs. PhD thesis, University of Edinburgh (1999)"},{"key":"50_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/BFb0037116","volume-title":"Typed Lambda Calculi and Applications","author":"C. Paulin-Mohring","year":"1993","unstructured":"Paulin-Mohring, C.: Inductive definitions in the system Coq: Rules and properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 328\u2013345. Springer, Heidelberg (1993)"},{"key":"50_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/10930755_8","volume-title":"Theorem Proving in Higher Order Logics","author":"C. Sch\u00fcrmann","year":"2003","unstructured":"Sch\u00fcrmann, C., Pfenning, F.: A coverage checking algorithm for LF. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 120\u2013135. Springer, Heidelberg (2003)"},{"key":"50_CR17","series-title":"Cambridge Tracts in Theoretical Computer Science","volume-title":"Term Rewriting Systems","author":"Terese","year":"2003","unstructured":"Terese.: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2003)"},{"key":"50_CR18","first-page":"76","volume-title":"Proc. of POPL 1984","author":"J.-J. Thiel","year":"1984","unstructured":"Thiel, J.-J.: Stop loosing sleep over incomplete specifications. In: Proc. of POPL 1984, pp. 76\u201382. ACM Press, New York (1984)"},{"issue":"2","key":"50_CR19","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1017\/S0956796802004641","volume":"13","author":"D. Walukiewicz-Chrz\u0105szcz","year":"2003","unstructured":"Walukiewicz-Chrz\u0105szcz, D.: Termination of rewriting in the calculus of constructions. Journal of Functional Programming\u00a013(2), 339\u2013414 (2003)","journal-title":"Journal of Functional Programming"},{"key":"50_CR20","doi-asserted-by":"crossref","unstructured":"Walukiewicz-Chrz\u0105szcz, D.: Termination of Rewriting in the Calculus of Constructions. PhD thesis, Warsaw University and University Paris XI (2003)","DOI":"10.1017\/S0956796802004641"},{"key":"50_CR21","unstructured":"Walukiewicz-Chrz\u0105szcz, D., Chrz\u0105szcz, J.: Consistency and completeness of rewriting in the calculus of constructions, available for download at http:\/\/www.mimuw.edu.pl\/homedirchrzaszcz\/papers\/"},{"key":"50_CR22","unstructured":"Werner, B.: M\u00e9ta-th\u00e9orie du Calcul des Constructions Inductives. PhD thesis, Universit\u00e9 Paris 7 (1994)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_50.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:14:38Z","timestamp":1605626078000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_50"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/11814771_50","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}