{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:00:43Z","timestamp":1725559243870},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642140518"},{"type":"electronic","value":"9783642140525"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_31","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T14:23:14Z","timestamp":1278944594000},"page":"450-465","source":"Crossref","is-referenced-by-count":0,"title":["Inductive Consequences in the Calculus of Constructions"],"prefix":"10.1007","author":[{"given":"Daria","family":"Walukiewicz-Chrz\u0105szcz","sequence":"first","affiliation":[]},{"given":"Jacek","family":"Chrz\u0105szcz","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"31_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-642-02273-9_3","volume-title":"Typed Lambda Calculi and Applications","author":"A. Abel","year":"2009","unstructured":"Abel, A., Coquand, T., Pagano, M.: A modular type-checking algorithm for type theory with singleton types and proof irrelevance. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol.\u00a05608, pp. 5\u201319. Springer, Heidelberg (2009)"},{"key":"31_CR2","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1145\/1292597.1292608","volume-title":"PLPV 2007","author":"T. Altenkirch","year":"2007","unstructured":"Altenkirch, T., McBride, C., Swierstra, W.: Observational equality, now? In: PLPV 2007, pp. 57\u201368. ACM, New York (2007)"},{"issue":"6","key":"31_CR3","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"},{"issue":"1","key":"31_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":"31_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":"31_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-540-74915-8_26","volume-title":"Computer Science Logic","author":"F. Blanqui","year":"2007","unstructured":"Blanqui, F., Jouannaud, J.P., Strub, P.Y.: Building decision procedures in the calculus of inductive constructions. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol.\u00a04646, pp. 328\u2013342. Springer, Heidelberg (2007)"},{"key":"31_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"130","DOI":"10.1007\/978-3-540-24849-1_9","volume-title":"Types for Proofs and Programs","author":"J. Chrz\u0105szcz","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":"31_CR8","unstructured":"Chrz\u0105szcz, J.: Modules in Type Theory with Generative Definitions. PhD thesis, Warsaw University and University Paris-Sud (2004)"},{"key":"31_CR9","unstructured":"The Coq proof assistant, http:\/\/coq.inria.fr\/"},{"key":"31_CR10","series-title":"EATCS Monographs on Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-69962-7","volume-title":"Fundamentals of Algebraic Specification 1. Equations and Initial Semantics","author":"H. Ehrig","year":"1985","unstructured":"Ehrig, H., Mahr, B.: Fundamentals of Algebraic Specification 1. Equations and Initial Semantics. EATCS Monographs on Theoretical Computer Science, vol.\u00a06. Springer, Heidelberg (1985)"},{"key":"31_CR11","first-page":"208","volume-title":"LICS 1994","author":"M. Hofmann","year":"1994","unstructured":"Hofmann, M., Streicher, T.: The groupoid model refutes uniqueness of identity proofs. In: LICS 1994, pp. 208\u2013212. IEEE Computer Society, Los Alamitos (1994)"},{"key":"31_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-39185-1_12","volume-title":"Types for Proofs and Programs","author":"P. Letouzey","year":"2003","unstructured":"Letouzey, P.: A new extraction for Coq. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol.\u00a02646, pp. 200\u2013219. Springer, Heidelberg (2003)"},{"key":"31_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.F. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 278\u2013293. Springer, Heidelberg (2005)"},{"key":"31_CR14","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":"31_CR15","series-title":"Cambridge Tracts in Theoretical Computer Science","volume-title":"Term Rewriting Systems","year":"2003","unstructured":"Terese (ed.): Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol.\u00a055. Cambridge University Press, Cambridge (2003)"},{"issue":"2","key":"31_CR16","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":"31_CR17","doi-asserted-by":"crossref","unstructured":"Walukiewicz-Chrz\u0105szcz, D.: Termination of Rewriting in the Calculus of Constructions. PhD thesis, Warsaw University and University Paris-Sud (2003)","DOI":"10.1017\/S0956796802004641"},{"key":"31_CR18","unstructured":"Walukiewicz-Chrz\u0105szcz, D., Chrz\u0105szcz, J.: Inductive consequences in the calculus of constructions, http:\/\/www.mimuw.edu.pl\/~chrzaszcz\/papers\/"},{"key":"31_CR19","doi-asserted-by":"crossref","unstructured":"Walukiewicz-Chrz\u0105szcz, D., Chrz\u0105szcz, J.: Consistency and completeness of rewriting in the calculus of constructions. Logical Methods of Computer Science\u00a04(3) (2008)","DOI":"10.2168\/LMCS-4(3:8)2008"},{"key":"31_CR20","doi-asserted-by":"crossref","unstructured":"Werner, B.: On the strength of proof-irrelevant type theories. Logical Methods in Computer Science\u00a04(3) (2008)","DOI":"10.2168\/LMCS-4(3:13)2008"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14052-5_31.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:47:03Z","timestamp":1606186023000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}