{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:35:39Z","timestamp":1759638939365,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662013"},{"type":"electronic","value":"9783540486855"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48685-2_25","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:13:41Z","timestamp":1269897221000},"page":"301-316","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":26,"title":["The Calculus of Algebraic Constructions"],"prefix":"10.1007","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Blanqui","sequence":"first","affiliation":[]},{"given":"Jean-Pierre","family":"Jouannaud","sequence":"additional","affiliation":[]},{"given":"Mitsuhiro","family":"Okada","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,11,5]]},"reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"F. Barbanera, M. Fern\u00e1ndez, and H. Geuvers. Modularity of strong normalization in the algebraic-\u03bb-cube. Journal of Functional Programming, 7(6), 1997.","DOI":"10.1017\/S095679689700289X"},{"key":"25_CR2","unstructured":"H. Barendregt. Introduction to generalized type systems. Journal of Functional Programming, 1992."},{"key":"25_CR3","unstructured":"F. Blanqui, J.-P. Jouannaud, and M. Okada. Inductive Data Type Systems, 1998."},{"key":"25_CR4","doi-asserted-by":"crossref","unstructured":"V. Breazu-Tannen. Combining algebra and higher-order types. In Third IEEE Annual Symposium on Logic in Computer Science, pages 82\u201390. 1988.","DOI":"10.1109\/LICS.1988.5103"},{"issue":"1","key":"25_CR5","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(91)90037-3","volume":"83","author":"V. Breazu-Tannen","year":"1991","unstructured":"V. Breazu-Tannen and J. Gallier. Polymorphic rewriting conserves algebraic strong normalization. Theoretical Computer Science, 83 (1):3\u201328, June 1991.","journal-title":"Theoretical Computer Science"},{"key":"25_CR6","unstructured":"T. Coquand. Pattern matching with dependent types. In B. Nordstr\u00f6m, K. Pettersson, G. Plotkin, editors, Workshop on Types for Proofs and Programs, 1992."},{"key":"25_CR7","unstructured":"T. Coquand and J. Gallier. A proof of strong normalization for the Theory of Constructions using a Kripke-like interpretation. 1st Intl. Workshop on Logical Frameworks. 1990."},{"key":"25_CR8","doi-asserted-by":"publisher","first-page":"96","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:96\u2013120, 1988.","journal-title":"Information and Computation"},{"key":"25_CR9","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of Colog\u201988","author":"T. Coquand","year":"1990","unstructured":"T. Coquand and C. Paulin-Mohring. Inductively defined types. In P. Martin-L\u00f6f and G. Mints, editors, Proceedings of Colog\u201988, LNCS 417. Springer-Verlag, 1990."},{"key":"25_CR10","unstructured":"C. Cornes. Conception d\u2019un langage de haut niveau de representation de preuves: R\u00e9currence par filtrage de motifs; Unification en pr\u00e9sence de types inductifs primitifs; Synth\u00e9se de lemmes d\u2019inversion. PhD thesis, Universit\u00e9 de Paris 7, 1997."},{"issue":"2","key":"25_CR11","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/S0304-3975(96)00121-1","volume":"169","author":"R. Cosmo Di","year":"1996","unstructured":"R. Di Cosmo and D. Kesner. Combining algebraic rewriting, extensional lambda calculi, and fixpoints. Theoretical Computer Science, 169(2):201\u2013220, 1996.","journal-title":"Theoretical Computer Science"},{"key":"25_CR12","unstructured":"J. Courant. A module calculus for Pure Type Systems. TLCA\u201997."},{"key":"25_CR13","unstructured":"G. Dowek, T. Hardin, and C. Kirchner. Theorem proving modulo. Technical Report 3400, INRIA, 1998."},{"key":"25_CR14","unstructured":"J. Gallier. On Girard\u2019s \u201cCandidats de R\u00e9ductibilit\u00e9\u201d. In P.-G. Odifreddi, editor, Logic and Computer Science. North Holland, 1990."},{"key":"25_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1007\/3-540-60579-7_2","volume-title":"Selected Papers 2nd Intl. Workshop on Types for Proofs and Programs, TYPES\u201994, B\u00e1stad, Sweden, 6-10 June 1994","author":"H. Geuvers","year":"1995","unstructured":"H. Geuvers. A short and flexible proof of strong normalization for the Calculus of Constructions. In P. Dybjer, B. Nordstr\u00f6m, and J. Smith, editors, Selected Papers 2nd Intl. Workshop on Types for Proofs and Programs, TYPES\u201994, B\u00e1stad, Sweden, 6-10 June 1994, volume 996 of LNCS, pages 14\u201338. 1995."},{"key":"25_CR16","unstructured":"J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1988."},{"issue":"2","key":"25_CR17","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1016\/S0304-3975(96)00161-2","volume":"173","author":"J.-P. Jouannaud","year":"1997","unstructured":"J.-P. Jouannaud and M. Okada. Abstract Data Type Systems. Theoretical Computer Science, 173(2):349\u2013391, February 1997.","journal-title":"Theoretical Computer Science"},{"issue":"1-2","key":"25_CR18","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(93)90091-7","volume":"121","author":"J. W. Klop","year":"1993","unstructured":"J. W. Klop, V. van Oostrom, and F. van Raamsdonk. Combinatory reduction systems: introduction and survey. Theoretical Computer Science, 121(1-2):279\u2013308, December 1993.","journal-title":"Theoretical Computer Science"},{"key":"25_CR19","doi-asserted-by":"crossref","unstructured":"T. Nipkow. Higher-order critical pairs. In Proc. 6th IEEE Symp. Logic in Computer Science, Amsterdam, pages 342\u2013349, 1991.","DOI":"10.1109\/LICS.1991.151658"},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"M. Okada. Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewrite system. In G. H. Gonnet, editor, Proceedings of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, pages 357\u2013363. ACM Press, July 1989.","DOI":"10.1145\/74540.74582"},{"key":"25_CR21","unstructured":"B. Werner. Une Th\u00e9orie des Constructions Inductives. Th\u00e9se, Universit\u00e9 Paris 7, 1994."}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48685-2_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T19:17:09Z","timestamp":1739992629000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48685-2_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662013","9783540486855"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-48685-2_25","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"5 November 1999","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}