{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:08:22Z","timestamp":1725664102267},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540582335"},{"type":"electronic","value":"9783540485797"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58233-9_14","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:38:18Z","timestamp":1330270698000},"page":"305-325","source":"Crossref","is-referenced-by-count":11,"title":["Termination proofs for higher-order rewrite systems"],"prefix":"10.1007","author":[{"given":"Jaco","family":"Pol","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"14_CR1","unstructured":"G.J. Akkerman and J.C.M. Baeten. Term rewriting analysis in process algebra. Technical Report CS-R9130, Centre for Mathematics and Computer Science, June 1991."},{"key":"14_CR2","volume-title":"The Lambda Calculus. Its Syntax and Semantics","author":"H.P. Barendregt","year":"1984","unstructured":"H.P. Barendregt. The Lambda Calculus. Its Syntax and Semantics. North-Holland, Amsterdam, second, revised edition, 1984.","edition":"second, revised"},{"key":"14_CR3","series-title":"volume 664 of Lecture Notes in Computer Science","volume-title":"Proceedings of the 1st International Conference on Typed Lambda Calculi and Applications, TLCA '93","year":"1993","unstructured":"M. Bezem and J.F. Groote, editors. Proceedings of the 1 st International Conference on Typed Lambda Calculi and Applications, TLCA '93, Utrecht, The Netherlands, volume 664 of Lecture Notes in Computer Science. Springer-Verlag, 1993."},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"V. Breazu-Tannen. Combining algebra and higher-order types. In Proceedings 3 th Annual Symposium on Logic in Computer Science, Edinburgh, pages 82\u201390, July 1988.","DOI":"10.1109\/LICS.1988.5103"},{"key":"14_CR5","unstructured":"R. de Vrijer. Surjective Pairing and Strong Normalization: Two Themes in Lambda Calculus. PhD thesis, University of Amsterdam, 1987."},{"key":"14_CR6","unstructured":"R.O. Gandy. Proofs of strong normalization. In J.R. Hindley and J.P. Seldin, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 457\u2013477. Academic Press, 1980."},{"key":"14_CR7","volume-title":"Report CS-R9076","author":"J.F. Groote","year":"1990","unstructured":"J.F. Groote and A. Ponse. The syntax and semantics of \u03bcCRL. Report CS-R9076, CWI, Amsterdam, 1990."},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"G. Huet and D.C. Oppen. Equations and rewrite rules: A survey. In R. Book, editor, Formal Language Theory: Perspectives and Open Problems, pages 349\u2013405. Academic Press, 1980.","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"J.P. Jouannaud and M. Okada. A computation model for executable higher-order algebraic specification languages. In Proceedings 6 th Annual Symposium on Logic in Computer Science, Amsterdam, The Netherlands, pages 350\u2013361, 1991.","DOI":"10.1109\/LICS.1991.151659"},{"key":"14_CR10","volume-title":"Technical Report CS-R9345","author":"Z. Khasidashvili","year":"1993","unstructured":"Z. Khasidashvili. Perpetual reductions and strong normalization in orthogonal term rewriting systems. Technical Report CS-R9345, CWI, Amsterdam, July 1993."},{"key":"14_CR11","volume-title":"volume 127 of Mathematical Centre Tracts","author":"J.W. Klop","year":"1980","unstructured":"J.W. Klop. Combinatory Reduction Systems, volume 127 of Mathematical Centre Tracts. Mathematisch Centrum, Amsterdam, 1980."},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"T. Nipkow. Higher-order critical pairs. In Proceedings 6 th Annual Symposium on Logic in Computer Science, Amsterdam, The Netherlands, pages 342\u2013349, 1991.","DOI":"10.1109\/LICS.1991.151658"},{"key":"14_CR13","series-title":"volume 664 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"306","DOI":"10.1007\/BFb0037114","volume-title":"Proceedings of the 1st International Conference on Typed Lambda Calculi and Applications, TLCA '93","author":"T. Nipkow","year":"1993","unstructured":"T. Nipkow. Orthogonal higher-order rewrite systems are confluent. In Bezem and Groote [3], pages 306\u2013317."},{"key":"14_CR14","series-title":"volume 664 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/BFb0037116","volume-title":"Proceedings of the 1st International Conference on Typed Lambda Calculi and Applications, TLCA '93","author":"C. Paulin-Mohring","year":"1993","unstructured":"C. Paulin-Mohring. Inductive definitions in the system Coq. Rules and properties. In Bezem and Groote [3], pages 328\u2013345."},{"key":"14_CR15","series-title":"The APIC-series 31","first-page":"361","volume-title":"Logic and Computer Science","author":"L. C. Paulson","year":"1990","unstructured":"L. C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361\u2013386. Academic Press Limited, London, 1990. In: The APIC-series 31."},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"M.P.A. Sellink. Verifying process algebra proofs in type theory. Technical Report 87, Logic Group Preprint Series, Utrecht University, March 1993.","DOI":"10.1007\/978-1-4471-3229-5_18"},{"key":"14_CR17","volume-title":"Technical Report IR-333","author":"V. Oostrom van","year":"1993","unstructured":"V. van Oostrom and F. van Raamsdonk. Comparing combinatory reduction systems and higher-order rewrite systems. Technical Report IR-333, Vrije Universiteit Amsterdam, August 1993. Appears in this Volume."},{"key":"14_CR18","volume-title":"volume 21 of Cambridge tracts in theoretical computer science","author":"D.A. Wolfram","year":"1993","unstructured":"D.A. Wolfram. The Clausal Theory of Types, volume 21 of Cambridge tracts in theoretical computer science. Cambridge University Press, Cambridge, 1993."},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"H. Zantema. Termination of term rewriting by interpretation. In M. Rusinowitch and J.L. R\u00e9my, editors, Conditional Term Rewriting Systems, proceedings third international workshop CTRS-92, volume 656 of Lecture Notes in Computer Science, pages 155\u2013167. Springer-Verlag, 1993. Full version appeared as report RUU-CS-92-14, Utrecht University.","DOI":"10.1007\/3-540-56393-8_12"}],"container-title":["Lecture Notes in Computer Science","Higher-Order Algebra, Logic, and Term Rewriting"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58233-9_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:18:56Z","timestamp":1605647936000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58233-9_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540582335","9783540485797"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-58233-9_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}