{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T14:10:43Z","timestamp":1778249443489,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540582335","type":"print"},{"value":"9783540485797","type":"electronic"}],"license":[{"start":{"date-parts":[[1994,1,1]],"date-time":"1994-01-01T00:00:00Z","timestamp":757382400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1994,1,1]],"date-time":"1994-01-01T00:00:00Z","timestamp":757382400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58233-9_2","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T10:38:12Z","timestamp":1330252692000},"page":"20-39","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Strong normalization of typeable rewrite systems"],"prefix":"10.1007","author":[{"given":"Steffen","family":"van Bakel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maribel","family":"Fern\u00e1ndez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0304-3975(92)90297-S","volume":"102","author":"S. van Bakel","year":"1992","unstructured":"S. van Bakel. Complete restrictions of the Intersection Type Discipline. Theoretical Computer Science, 102:135\u2013163, 1992.","journal-title":"Theoretical Computer Science"},{"key":"2_CR2","unstructured":"S. van Bakel. Partial Intersection Type Assignment of Rank 2 in Applicative Term Rewriting Systems. Technical Report 92-03, Department of Computer Science, University of Nijmegen, 1992."},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"S. van Bakel. Essential Intersection Type Assignment. In R.K. Shyamasunda, editor, Proceedings of FST&TCS '93. 13\n\n                  th\n                \nConference on Foundations of Software Technology and Theoretical Computer Science, LNCS 761, pages 13\u201323, Bombay, India, 1993.","DOI":"10.1007\/3-540-57529-4_40"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"S. van Bakel. Partial Intersection Type Assignment in Applicative Term Rewriting Systems. In M. Bezem and J.F. Groote, editors, Proceedings of TLCA '93. International Conference on Typed Lambda Calculi and Applications, LNCS 664, pages 29\u201344, Utrecht, the Netherlands, 1993.","DOI":"10.1007\/BFb0037096"},{"issue":"6","key":"2_CR5","doi-asserted-by":"crossref","first-page":"643","DOI":"10.1093\/logcom\/3.6.643","volume":"3","author":"S. van Bakel","year":"1993","unstructured":"S. van Bakel. Principal type schemes for the Strict Type Assignment System. Logic and Computation, 3(6):643\u2013670, 1993.","journal-title":"Logic and Computation"},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"F. Barbanera and M. Fern\u00e1ndez. Combining first and higher order rewrite systems with type assignment systems. In M. Bezem and J.F. Groote, editors, Proceedings of TLCA '93. International Conference on Typed Lambda Calculi and Applications, LNCS 664, pages 60\u201374, Utrecht, the Netherlands, 1993.","DOI":"10.1007\/BFb0037098"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"F. Barbanera and M. Fern\u00e1ndez. Modularity of Termination and Confluence in Combinations of Rewrite Systems with \u03bb\n\u03c9. In A. Lingas, R. Karlsson, and S. Carlsson, editors, Proceedings of ICALP '93. 20\n\n                  th\n                \nInternational Colloquium on Automata, Languages and Programming, LNCS 700, pages 657\u2013668, Lund, Sweden, 1993.","DOI":"10.1007\/3-540-56939-1_110"},{"key":"2_CR8","volume-title":"The Lambda Calculus: its Syntax and Semantics","author":"H. Barendregt","year":"1984","unstructured":"H. Barendregt. The Lambda Calculus: its Syntax and Semantics. North-Holland, Amsterdam, revised edition, 1984.","edition":"revised edition"},{"issue":"4","key":"2_CR9","doi-asserted-by":"crossref","first-page":"931","DOI":"10.2307\/2273659","volume":"48","author":"H. Barendregt","year":"1983","unstructured":"H. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48(4):931\u2013940, 1983.","journal-title":"Journal of Symbolic Logic"},{"key":"2_CR10","first-page":"535","volume-title":"To H.B. Curry, Essays in combinatory logic, lambda-calculus and formalism","author":"M. Coppo","year":"1980","unstructured":"M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Principal type schemes and \u03bb-calculus semantics. In J.R. Hindley and J.P. Seldin, editors, To H.B. Curry, Essays in combinatory logic, lambda-calculus and formalism, pages 535\u2013560. Academic press, New York, 1980."},{"key":"2_CR11","volume-title":"Combinatory Logic, volume 1","author":"H.B. Curry","year":"1958","unstructured":"H.B. Curry and R. Feys. Combinatory Logic, volume 1. North-Holland, Amsterdam, 1958."},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and J.P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 6, pages 245\u2013320. North-Holland, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"2_CR13","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1016\/0304-3975(92)90306-Z","volume":"100","author":"M. Dezani-Ciancaglini","year":"1992","unstructured":"M. Dezani-Ciancaglini and J.R. Hindley. Intersection types for combinatory logic. Theoretical Computer Science, 100:303\u2013324, 1992.","journal-title":"Theoretical Computer Science"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"K. Futatsugi, J. Goguen, J.P. Jouannaud, and J. Meseguer. Principles of OBJ2. In Proceedings 12\n\n                  th\n                \nACM Symposium on Principles of Programming Languages, pages 52\u201366, 1985.","DOI":"10.1145\/318593.318610"},{"key":"2_CR15","unstructured":"J.Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989."},{"key":"2_CR16","first-page":"29","volume":"146","author":"J.R. Hindley","year":"1969","unstructured":"J.R. Hindley. The principal type scheme of an object in combinatory logic. Transactions of the American Mathematical Society, 146:29\u201360, 1969.","journal-title":"Transactions of the American Mathematical Society"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"J.P. Jouannaud and M. Okada. Executable higher-order algebraic specification languages. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science, pages 350\u2013361, 1991.","DOI":"10.1109\/LICS.1991.151659"},{"key":"2_CR18","unstructured":"J.W. Klop. Term Rewriting Systems. In S. Abramsky, Dov.M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, chapter 1, pages 1\u2013116. Clarendon Press, 1992."},{"key":"2_CR19","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R. Milner","year":"1978","unstructured":"R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348\u2013375, 1978.","journal-title":"Journal of Computer and System Sciences"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"F. Pfenning. Partial Polymorphic Type Inference and Higher-Order Unification. In Proceedings of the 1988 ACM conference on LISP and Functional Programming Languages, pages 153\u2013163, 1988.","DOI":"10.1145\/62678.62697"},{"key":"2_CR21","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1016\/0304-3975(83)90069-5","volume":"28","author":"S. Ronchi della Rocca","year":"1984","unstructured":"S. Ronchi della Rocca and B. Venneri. Principal type schemes for an extended type theory. Theoretical Computer Science, 28:151\u2013169, 1984.","journal-title":"Theoretical Computer Science"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"W.W. Tait. Intensional interpretation of functional of finite types. Journal of Symbolic Logic, 32, 1967.","DOI":"10.2307\/2271658"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"D.A. Turner. Miranda: A non-strict functional language with polymorphic types. In Proceedings of the conference on Functional Programming Languages and Computer Architecture, LNCS 201, pages 1\u201316.","DOI":"10.1007\/3-540-15975-4_26"}],"container-title":["Lecture Notes in Computer Science","Higher-Order Algebra, Logic, and Term Rewriting"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58233-9_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T13:16:02Z","timestamp":1778246162000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-58233-9_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540582335","9783540485797"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-58233-9_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994]]},"assertion":[{"value":"7 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}