{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:32:45Z","timestamp":1759638765685},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540677789"},{"type":"electronic","value":"9783540449805"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10721975_4","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T15:43:04Z","timestamp":1167406984000},"page":"47-61","source":"Crossref","is-referenced-by-count":25,"title":["Termination and Confluence of Higher-Order Rewrite Systems"],"prefix":"10.1007","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Blanqui","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","unstructured":"Aczel, P.: A general Church-Rosser theorem. Technical report, University of Manchester, United Kingdom (1978)"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Barbanera, F., Fern\u00e1ndez, M., Geuvers, H.: Modularity of strong normalization in the algebraic-\u03bb-cube. Journal of Functional Programming\u00a07(6) (1997)","DOI":"10.1017\/S095679689700289X"},{"key":"4_CR3","volume-title":"Handbook of logic in computer science","author":"H. Barendregt","year":"1992","unstructured":"Barendregt, H.: Lambda calculi with types. In: Abramski, S., Gabbai, D.M., Maiboum, T.S.E. (eds.) Handbook of logic in computer science, vol.\u00a02, Oxford University Press, Oxford (1992)"},{"key":"4_CR4","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, p. 301. Springer, Heidelberg (1999)"},{"key":"4_CR5","unstructured":"Blanqui, F., Jouannaud, J.-P., Okada, M.: Inductive Data Type Systems (1998), To appear in TCS, Available at \n                    \n                      http:\/\/www.lri.fr\/~blanqui\/"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Breazu-Tannen, V.: Combining algebra and higher-order types. In: Proc. of LICS 1988, IEEE Computer Society, Los Alamitos (1988)","DOI":"10.1109\/LICS.1988.5103"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Automata, Languages and Programming","author":"V. Breazu-Tannen","year":"1989","unstructured":"Breazu-Tannen, V., Gallier, J.: Polymorphic rewriting conserves algebraic strong normalization. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol.\u00a0372, Springer, Heidelberg (1989)"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Breazu-Tannen, V., Gallier, J.: Polymorphic rewriting conserves algebraic strong normalization. Theoretical Computer Science\u00a083(1) (1991)","DOI":"10.1016\/0304-3975(91)90037-3"},{"key":"4_CR9","unstructured":"Hindley, J.R., Seldin, J.P.: Introduction to combinators and \u03bb-calculus. London Mathematical Society (1986)"},{"key":"4_CR10","unstructured":"INRIA-Rocquencourt\/CNRS\/Universit\u00e9 Paris-Sud\/ENS Lyon, France. The Coq Proof Assistant Reference Manual Version 6.3 (1999), Available at \n                    \n                      http:\/\/pauillac.inria.fr\/coq\/"},{"key":"4_CR11","volume-title":"Proc. of LICS 1991","author":"J.-P. Jouannaud","year":"1991","unstructured":"Jouannaud, J.-P., Okada, M.: Executable higher-order algebraic specification languages. In: Proc. of LICS 1991, IEEE Computer Society, Los Alamitos (1991)"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Jouannaud, J.-P., Okada, M.: Abstract Data Type Systems. Theoretical Computer Science\u00a0173(2) (1997)","DOI":"10.1016\/S0304-3975(96)00161-2"},{"key":"4_CR13","volume-title":"Proc. of LICS 1999","author":"J.-P. Jouannaud","year":"1999","unstructured":"Jouannaud, J.-P., Rubio, A.: The Higher-Order Recursive Path Ordering. In: Proc. of LICS 1999, IEEE Computer Society, Los Alamitos (1999)"},{"key":"4_CR14","unstructured":"Khasidashvili, Z.: Expression Reduction Systems. In: Proc. of I. Vekua Institute of Applied Mathematics, vol.\u00a036 (1990)"},{"key":"4_CR15","unstructured":"Klop, J.W.: Combinatory Reduction Systems. PhD thesis, University of Utrecht, Netherlands (1980), Published as Mathematical Center Tract 129"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Klop, J.W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: introduction and survey. Theoretical Computer Science\u00a0121(1-2) (1993)","DOI":"10.1016\/0304-3975(93)90091-7"},{"key":"4_CR17","volume-title":"LEGO Proof Development System: User\u2019s manual","author":"Z. Luo","year":"1992","unstructured":"Luo, Z., Pollack, R.: LEGO Proof Development System: User\u2019s manual. University of Edinburgh, Scotland (1992)"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. Theoretical Computer Science, 192 (1998)","DOI":"10.1016\/S0304-3975(97)00143-6"},{"key":"4_CR19","unstructured":"Mendler, N. P.: Inductive Definition in Type Theory. PhD thesis, Cornell University, United States (1987)"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0038698","volume-title":"Extensions of Logic Programming","author":"D. Miller","year":"1991","unstructured":"Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. In: Schroeder-Heister, P. (ed.) ELP 1989. LNCS, vol.\u00a0475, Springer, Heidelberg (1991)"},{"key":"4_CR21","unstructured":"Miller, D., Nadathur, G.: An overview of \u03bbProlog. In: Proc. of the 5th Int. Conf. on Logic Programming (1988)"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"M\u00fcller, F.: Confluence of the lambda calculus with left-linear algebraic rewriting. Information Processing Letters\u00a041 (1992)","DOI":"10.1016\/0020-0190(92)90155-O"},{"key":"4_CR23","volume-title":"Proc. of LICS 1991","author":"T. Nipkow","year":"1991","unstructured":"Nipkow, T.: Higher-order critical pairs. In: Proc. of LICS 1991, IEEE Computer Society, Los Alamitos (1991)"},{"key":"4_CR24","volume-title":"Proc. of ISSAC 1989","author":"M. Okada","year":"1989","unstructured":"Okada, M.: Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewrite system. In: Proc. of ISSAC 1989, ACM Press, New York (1989)"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle","author":"L. Paulson","year":"1994","unstructured":"Paulson, L.: Isabelle: a generic theorem prover. In: Paulson, L.C. (ed.) Isabelle. LNCS, vol.\u00a0828, Springer, Heidelberg (1994)"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Tait, W.W.: Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic\u00a032(2) (1967)","DOI":"10.2307\/2271658"},{"key":"4_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037121","volume-title":"Typed Lambda Calculi and Applications","author":"M. Takahashi","year":"1993","unstructured":"Takahashi, M.: \u03bb-calculi with conditional rules. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, Springer, Heidelberg (1993)"},{"key":"4_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014064","volume-title":"Typed Lambda Calculi and Applications","author":"J. Pol van de","year":"1995","unstructured":"van de Pol, J., Schwichtenberg, H.: Strict functionals for termination proofs. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol.\u00a0902, Springer, Heidelberg (1995)"},{"key":"4_CR29","unstructured":"van Oostrom, V.: Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Netherlands (1994)"},{"key":"4_CR30","series-title":"Lecture Notes in Computer Science","volume-title":"Higher-Order Algebra, Logic, and Term Rewriting","author":"V. Oostrom van","year":"1996","unstructured":"van Oostrom, V.: Development closed critical pairs. In: Dowek, G., Heering, J., Meinke, K., M\u00f6ller, B. (eds.) HOA 1995. LNCS, vol.\u00a01074, Springer, Heidelberg (1996)"},{"key":"4_CR31","series-title":"Lecture Notes in Computer Science","volume-title":"Higher-Order Algebra, Logic, and Term Rewriting","author":"V. Oostrom van","year":"1994","unstructured":"van Oostrom, V., van Raamsdonk, F.: Comparing Combinatory Reduction Systems and Higher-order Rewrite Systems. In: Heering, J., Meinke, K., M\u00f6ller, B., Nipkow, T. (eds.) HOA 1993. LNCS, vol.\u00a0816, Springer, Heidelberg (1994)"},{"key":"4_CR32","unstructured":"van Raamsdonk, F.: Confluence and Normalization for Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Netherlands (1996)"},{"key":"4_CR33","unstructured":"Wolfram, D.: The clausal theory of types. PhD thesis, University of Cambridge, United Kingdom (1990)"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10721975_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,23]],"date-time":"2019-03-23T05:34:57Z","timestamp":1553319297000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10721975_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540677789","9783540449805"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/10721975_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}