{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:28:08Z","timestamp":1725550088260},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642119989"},{"type":"electronic","value":"9783642119996"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11999-6_5","type":"book-chapter","created":{"date-parts":[[2010,3,16]],"date-time":"2010-03-16T04:52:29Z","timestamp":1268715149000},"page":"62-78","source":"Crossref","is-referenced-by-count":6,"title":["Semantic Labelling for Proving Termination of Combinatory Reduction Systems"],"prefix":"10.1007","author":[{"given":"Makoto","family":"Hamana","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","unstructured":"Aczel, P.: A general Church-Rosser theorem. Technical report, University of Manchester (1978)"},{"key":"5_CR2","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/S0304-3975(00)00347-9","volume":"272","author":"F. Blanqui","year":"2002","unstructured":"Blanqui, F., Jouannaud, J.-P., Okada, M.: Inductive data type systems. Theoretical Computer Science\u00a0272, 41\u201368 (2002)","journal-title":"Theoretical Computer Science"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-87531-4_1","volume-title":"Computer Science Logic","author":"F. Blanqui","year":"2008","unstructured":"Blanqui, F., Jouannaud, J.-P., Rubio, A.: The computability path ordering: The end of a quest. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol.\u00a05213, pp. 1\u201314. Springer, Heidelberg (2008)"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/10721975_4","volume-title":"Rewriting Techniques and Applications","author":"F. Blanqui","year":"2000","unstructured":"Blanqui, F.: Termination and confluence of higher-order rewrite systems. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol.\u00a01833, pp. 47\u201361. Springer, Heidelberg (2000)"},{"key":"5_CR5","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"5_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/3-540-45653-8_37","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C. Borralleras","year":"2001","unstructured":"Borralleras, C., Rubio, A.: A monotonic higher-order semantic path ordering. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, pp. 531\u2013547. Springer, Heidelberg (2001)"},{"key":"5_CR7","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":"5_CR8","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, pp. 286\u2013301. Springer, Heidelberg (1998)"},{"key":"5_CR9","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":"5_CR10","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":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/978-3-540-32033-3_11","volume-title":"Term Rewriting and Applications","author":"M. Hamana","year":"2005","unstructured":"Hamana, M.: Universal algebra for termination of higher-order rewriting. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 135\u2013149. Springer, Heidelberg (2005)"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Hamana, M.: Higher-order semantic labelling for inductive datatype systems. In: Ninth ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP 2007), pp. 97\u2013108 (2007)","DOI":"10.1145\/1273920.1273933"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/11805618_29","volume-title":"Term Rewriting and Applications","author":"J.-P. Jouannaud","year":"2006","unstructured":"Jouannaud, J.-P., Rubio, A.: Higher-order orderings for normal rewriting. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, pp. 387\u2013399. Springer, Heidelberg (2006)"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Jouannaud, J.-P., Rubio, A.: Polymorphic higher-order recursive path orderings. Journal of ACM\u00a054(1) (2007)","DOI":"10.1145\/1206035.1206037"},{"key":"5_CR15","unstructured":"Jones, S.P., Tolmach, A., Hoare, T.: Playing by the rules: rewriting as a practical optimisation technique in GHC. In: Haskell Workshop 2001 (2001)"},{"key":"5_CR16","unstructured":"Klop, J.W.: Combinatory Reduction Systems. PhD thesis, CWI, Amsterdam. Mathematical Centre Tracts, vol.\u00a0127 (1980)"},{"issue":"1&2","key":"5_CR17","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":"5_CR18","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":"5_CR19","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Higher-order critical pairs. In: Proc. 6th IEEE Symp. Logic in Computer Science, pp. 342\u2013349 (1991)","DOI":"10.1109\/LICS.1991.151658"},{"key":"5_CR20","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":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/3-540-45127-7_20","volume-title":"Rewriting Techniques and Applications","author":"F. Raamsdonk van","year":"2001","unstructured":"van Raamsdonk, F.: On termination of higher-order rewriting. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol.\u00a02051, pp. 261\u2013275. Springer, Heidelberg (2001)"},{"key":"5_CR22","series-title":"Cambridge Tracts in Theoretical Computer Science","volume-title":"Term Rewriting Systems","author":"Terese","year":"2003","unstructured":"Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol.\u00a055. Cambridge University Press, Cambridge (2003)"},{"issue":"1\/2","key":"5_CR23","doi-asserted-by":"crossref","first-page":"89","DOI":"10.3233\/FI-1995-24124","volume":"24","author":"H. Zantema","year":"1995","unstructured":"Blanqui, F.: Termination and confluence of higher-order rewrite systems. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol.\u00a01833, pp. 47\u201361. Springer, Heidelberg (2000)","journal-title":"Fundamenta Informaticae"}],"container-title":["Lecture Notes in Computer Science","Functional and Constraint Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11999-6_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:46:15Z","timestamp":1606185975000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11999-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642119989","9783642119996"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11999-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}