{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:04:15Z","timestamp":1725566655816},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540255963"},{"type":"electronic","value":"9783540320333"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32033-3_11","type":"book-chapter","created":{"date-parts":[[2010,9,28]],"date-time":"2010-09-28T00:20:02Z","timestamp":1285633202000},"page":"135-149","source":"Crossref","is-referenced-by-count":11,"title":["Universal Algebra for Termination of Higher-Order Rewriting"],"prefix":"10.1007","author":[{"given":"Makoto","family":"Hamana","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","unstructured":"Aczel, P.: A general Church-Rosser theorem. Technical report, University of Manchester (1978)"},{"key":"11_CR2","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N. Bruijn de","year":"1972","unstructured":"de Bruijn, N.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indagationes Mathematicae\u00a034, 381\u2013391 (1972)","journal-title":"Indagationes Mathematicae"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/BFb0052377","volume-title":"Rewriting Techniques and Applications","author":"O. Danvy","year":"1998","unstructured":"Danvy, O., Rose, K.H.: Higher-order rewriting and partial evaluation. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol.\u00a01379, p. 286. Springer, Heidelberg (1998)"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding. In: Proc. 14th Annual Symposium on Logic in Computer Science, pp. 193\u2013202 (1999)","DOI":"10.1109\/LICS.1999.782615"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Hamana, M.: Term rewriting with variable binding: An initial algebra approach. In: Fifth ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP 2003), pp. 148\u2013159 (2003)","DOI":"10.1145\/888251.888266"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-540-30477-7_23","volume-title":"Programming Languages and Systems","author":"M. Hamana","year":"2004","unstructured":"Hamana, M.: Free \u03a3-monoids: A higher-order syntax with metavariables. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol.\u00a03302, pp. 348\u2013363. Springer, Heidelberg (2004)"},{"key":"11_CR7","unstructured":"Jouannaud, J.-P., Rubio, A.: Higher-order recursive path orderings \u00e0 la carte. In: International Workshop on Rewriting in Proof and Computation (RPC 2001), pp. 161\u2013175 (2001)"},{"key":"11_CR8","unstructured":"Klop, J.W.: Combinatory Reduction Systems. PhD thesis, CWI, Amsterdam, vol.127 of Mathematical Centre Tracts (1980)"},{"issue":"1&2","key":"11_CR9","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(93)90091-7","volume":"121","author":"J.W. Klop","year":"1993","unstructured":"Klop, J.W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: Introduction and survey. Theor. Comput. Sci.\u00a0121(1&2), 279\u2013308 (1993)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1007\/3-540-59200-8_65","volume-title":"Rewriting Techniques and Applications","author":"P. Lescanne","year":"1995","unstructured":"Lescanne, P., Rouyer-Degli, J.: Explicit substitutions with de Bruijn\u2019s levels. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol.\u00a0914, pp. 294\u2013308. Springer, Heidelberg (1995)"},{"key":"11_CR11","series-title":"Graduate Texts in Mathematics","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-9839-7","volume-title":"Categories for the Working Mathematician","author":"S. Mac Lane","year":"1971","unstructured":"Mac Lane, S.: Categories for the Working Mathematician. Graduate Texts in Mathematics, vol.\u00a05. Springer, New York (1971)"},{"key":"11_CR12","unstructured":"van Oostrom, V.: Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam (1994)"},{"key":"11_CR13","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":"11_CR14","unstructured":"Plotkin, G.: Binding algebras: A step between universal algebra and type theory (invited talk). In: Rewriting Techniques and Applications, 9th International Conference, RTA 1998, Tsukuba, Japan (1998)"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","first-page":"305","volume-title":"Higher-Order Algebra, Logic, and Term Rewriting","author":"J. Pol van de","year":"1994","unstructured":"van de Pol, J.: Termination proofs for higher-order rewrite systems. In: Heering, J., Meinke, K., M\u00f6ller, B., Nipkow, T. (eds.) HOA 1993. LNCS, vol.\u00a0816, pp. 305\u2013325. Springer, Heidelberg (1994)"},{"key":"11_CR16","unstructured":"van de Pol, J.: Termination of Higher-order Rewrite Systems. PhD thesis, Universiteit Utrecht (1996)"},{"key":"11_CR17","unstructured":"van Raamsdonk, F.: Examples of higher-order rewriting systems, at \n                  \n                    http:\/\/www.cs.vu.nl\/~femke\/ps\/"},{"key":"11_CR18","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1006\/jsco.1994.1003","volume":"17","author":"H. Zantema","year":"1994","unstructured":"Zantema, H.: Termination of term rewriting: interpretation and type elimination. Journal of Symbolic Computation\u00a017, 23\u201350 (1994)","journal-title":"Journal of Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Term Rewriting and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32033-3_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:45:32Z","timestamp":1620013532000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32033-3_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540255963","9783540320333"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32033-3_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}