{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,15]],"date-time":"2026-06-15T23:54:05Z","timestamp":1781567645188,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540634591","type":"print"},{"value":"9783540695554","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0027010","type":"book-chapter","created":{"date-parts":[[2005,11,19]],"date-time":"2005-11-19T10:34:01Z","timestamp":1132396441000},"page":"174-193","source":"Crossref","is-referenced-by-count":2,"title":["Termination of algebraic type systems: The syntactic approach"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Baxthe","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Femke","family":"van Raamsdonk","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,6,20]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"F. Baxbanera and M. FernSndez. Combining first and higher order rewrite systems with type assignment systems. In M.Bezem and J.-F. Groote, editors, Proceedings of TLCA'93, volume 664 of Lecture Notes in Computer Science, pages 60\u201374. Springer-Verlag,1993.","DOI":"10.1007\/BFb0037098"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"F. Barbanera and M. FernSndez. Modularity of termination and confluence in combinations of rewrite systems with \u03bb\u03c9 In A. Lingas, R. Karlsson, and S. Karlsson, editors, Proceedings of ICALP'93, volume 700 of Lecture Notes in Computer Science, pages 657\u2013668. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56939-1_110"},{"issue":"1\u20132","key":"12_CR3","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/S0304-3975(96)80706-7","volume":"170","author":"F. Barbanera","year":"1996","unstructured":"F. Barbanera and M. Fern\u00e1ndez. Intersection type assignment systems with higherorder algebraic rewriting. Theoretical Computer Science, 170(1\u20132):173\u2013207, 15 December 1996.","journal-title":"Theoretical Computer Science"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"F. Barbanera, M. Fern\u00e1ndez, and H. Geuvers. Modularity of strong normalisation and confluence in the algebraic \u03bb-cube. In Proceedings of LICS'94, pages 406\u2013415. IEEE Computer Society Press, 1994.","DOI":"10.1109\/LICS.1994.316049"},{"key":"12_CR5","unstructured":"H. Barendregt. Lambda calculi with types. In S. Abramsky, D. M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, pages 117\u2013309. Oxford Science Publications, 1992. Volume 2."},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"G. Baxthe and H. Geuvers. Congruence types. In H. Kleine Buening, editor, Proceedings of CSL'95, volume 1092 of Lecture Notes in Computer Science, pages 36\u201351. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61377-3_30"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"G. Baxthe and H. Geuvers. Modular properties of algebraic type systems. In G. Dowek, J. Heering, K. Meinke, and B. M\u00f6ller, editors, Proceedings of HOA'95, volume 1074 of Lecture Notes in Computer Science, pages 37\u201356. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61254-8_18"},{"key":"12_CR8","unstructured":"G. Barthe, J. Hatcliff, and M.H. S\u00f8rensen. Weak Normalization implies Strong Normalization in Generalized Non-Dependent Pure Type Systems. Draft, 1997."},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"G. Barthe and P.-A. Melli\u00e8s. On the subject reduction property for algebraic type systems. Proceedings of CSL'96. To appear as LNCS, 1996.","DOI":"10.1007\/3-540-63172-0_31"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"G. Barthe, M. Ruys, and H. Barendregt. A two-level approach towards lean proofchecking. In S. Berardi and M. Coppo, editors, Proceedings of TYPES'95, volume 1158 of Lecture Notes in Computer Science, pages 16\u201335. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61780-9_59"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"V. Breazu-Tannen. Combining algebra and higher-order types. In Proceedings of LICS'88, pages 82\u201390. IEEE Computer Society Press, 1988.","DOI":"10.1109\/LICS.1988.5103"},{"key":"12_CR12","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(91)90037-3","volume":"83","author":"V. Breazu-Tannen","year":"1990","unstructured":"V. Breazu-Tannen and J. Gallier. Polymorphic rewriting conserves algebraic strong normalisation. Theoretical Computer Science, 83:3\u201328, 1990.","journal-title":"Theoretical Computer Science"},{"issue":"2\/3","key":"12_CR13","doi-asserted-by":"crossref","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, February\/March 1988.","journal-title":"Information and Computation"},{"key":"12_CR14","unstructured":"R. Di Cosmo. A brief history of rewriting with extensionality. In F. Kamareddine, editor, International Summer School on Type Theory and Term Rewriting, Glasgow, September 1996. Kluwer, 199x. To appear."},{"issue":"2","key":"12_CR15","doi-asserted-by":"crossref","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, 5 December 1996.","journal-title":"Theoretical Computer Science"},{"key":"12_CR16","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1016\/0890-5401(92)90064-M","volume":"101","author":"D. Dougherty","year":"1992","unstructured":"D. Dougherty. Adding algebraic rewriting to the untyped lambda calculus. Information and Computation, 101:251\u2013267, 1992.","journal-title":"Information and Computation"},{"key":"12_CR17","unstructured":"M. Fernandez. Mod\u00e8les de calcul multiparadigmes fond\u00e8s sur la r\u00e9\u00e9criture. PhD thesis, Universit\u00e9 Paris-Sud Orsay, 1993."},{"key":"12_CR18","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","volume":"1","author":"H. Geuvers","year":"1991","unstructured":"H. Geuvers and M.-J. Nederhof. A modular proof of strong normalisation for the Calculus of Constructions. Journal of Functional Programming, 1:155\u2013189, 1991.","journal-title":"Journal of Functional Programming"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"J.-P. Jouannaud and M. Okada. Executable higher-order algebraic specification languages.In Proceedings of LICS'91, pages 350\u2013361. IEEE Computer Society Press, 1991.","DOI":"10.1109\/LICS.1991.151659"},{"issue":"2","key":"12_CR20","doi-asserted-by":"crossref","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, 1997.","journal-title":"Theoretical Computer Science"},{"key":"12_CR21","unstructured":"J.W. Klop. Combinatory reduction systems. Number 127 in Mathematical Centre Tracts. CWI, 1980."},{"key":"12_CR22","unstructured":"J.W. Klop. Term-rewriting systems. In S. Abramsky, D. M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, pages 1\u2013116. Oxford Science Publications, 1992. Volume 2."},{"key":"12_CR23","unstructured":"K. Meinke and J.V. Tucker, editors. Many sorted logic and its applications. John Wiley and Sons, 1993."},{"key":"12_CR24","unstructured":"J. van de Pol. Termination of higher-order rewrite systems. PhD thesis, University of Utrecht, 1996."},{"issue":"1","key":"12_CR25","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1006\/jsco.1994.1003","volume":"17","author":"H. Zantema","year":"1994","unstructured":"H. Zantema. Termination of term rewriting: Interpretation and type elimination. Journal of Symbolic Computation, 17(1):23\u201350, January 1994.","journal-title":"Journal of Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Algebraic and Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0027010","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,5]],"date-time":"2025-01-05T19:12:30Z","timestamp":1736104350000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0027010"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540634591","9783540695554"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/bfb0027010","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997]]}}}