{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,13]],"date-time":"2026-10-13T11:19:51Z","timestamp":1791890391774,"version":"4.3.4"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540612544","type":"print"},{"value":"9783540683896","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61254-8_17","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:20:33Z","timestamp":1330291233000},"page":"17-36","source":"Crossref","is-referenced-by-count":1,"title":["Approximation and normalization results for typeable term rewriting systems"],"prefix":"10.1007","author":[{"given":"Steffen","family":"Bakel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Maribel","family":"Fern\u00e1ndez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"2_CR1","first-page":"543","volume":"789","author":"Z. Ariola","year":"1994","unstructured":"Z. Ariola, R. Kennaway, J.W. Klop, R. Sleep, and F-J. de Vries. Syntactic definitions of undefined: on defining the undefined. In TACS '94, LNCS, 789, pages 543\u2013554, 1994.","journal-title":"LNCS"},{"key":"2_CR2","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0304-3975(92)90297-S","volume":"102","author":"S. Bakel van","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_CR3","first-page":"29","volume":"664","author":"S. Bakel van","year":"1993","unstructured":"S. van Bakel. Partial Intersection Type Assignment in Applicative Term Rewriting Systems. In TLCA '93, LNCS 664, pages 29\u201344, 1993.","journal-title":"LNCS"},{"issue":"6","key":"2_CR4","doi-asserted-by":"crossref","first-page":"643","DOI":"10.1093\/logcom\/3.6.643","volume":"3","author":"S. Bakel van","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_CR5","doi-asserted-by":"crossref","unstructured":"S. van Bakel. Rank 2 Intersection Type Assignment in Term Rewriting Systems. Fundamenta Informaticae, 1996. To appear.","DOI":"10.3233\/FI-1996-26204"},{"key":"2_CR6","first-page":"20","volume":"816","author":"S. Bakel van","year":"1994","unstructured":"S. van Bakel and M. Fern\u00e1ndez. Strong Normalization of Typeable Rewrite Systems. In HOA '93, LNCS 816, pages 20\u201339, 1994.","journal-title":"LNCS"},{"key":"2_CR7","first-page":"279","volume":"914","author":"S. Bakel van","year":"1995","unstructured":"S. van Bakel and M. Fern\u00e1ndez. (Head)-Normalization of Typeable Rewrite Systems. RTA '95, LNCS 914, pages 279\u2013293, 1995.","journal-title":"LNCS"},{"issue":"4","key":"2_CR8","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_CR9","unstructured":"F. Cardone and M. Coppo. Two Extensions of Curry's Type Inference System. In Logic and Computer Science, pages 19\u201375, 1990."},{"issue":"4","key":"2_CR10","doi-asserted-by":"crossref","first-page":"685","DOI":"10.1305\/ndjfl\/1093883253","volume":"21","author":"M. Coppo","year":"1980","unstructured":"M. Coppo and M. Dezani-Ciancaglini. An Extension of the Basic Functionality Theory for the \u03bb-Calculus. Notre Dame Journal of Formal Logic, 21(4):685\u2013693, 1980.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"2_CR11","unstructured":"H.B. Curry and R. Feys. Combinatory Logic, volume 1, 1958."},{"key":"2_CR12","first-page":"245","volume":"B","author":"N. Dershowitz","year":"1990","unstructured":"N. Dershowitz and J.P. Jouannaud. Rewrite systems. In Handbook of Theoretical Computer Science, volume B, chapter 6, pages 245\u2013320, 1990.","journal-title":"Handbook of Theoretical Computer Science"},{"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","unstructured":"J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science, 1989."},{"key":"2_CR15","unstructured":"G. Huet and J.J. L\u00e9vy. Computations in Orthogonal Rewriting Systems. In Computational Logic. Essays in Honour of Alan Robinson, 1991."},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"J.P. Jouannaud and M. Okada. Executable higher-order algebraic specification languages. In LiCS '91, pages 350\u2013361, 1991.","DOI":"10.1109\/LICS.1991.151659"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"R. Kennaway, V. van Oostrom, and F.J. de Vries. Meaningless terms in rewriting. Submitted for publication. Obtainable as: http:\/\/wwwbroy.informatik.tumuenchen.de\/oostrom, 1996.","DOI":"10.1007\/3-540-61735-3_17"},{"key":"2_CR18","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1093\/logcom\/2.1.1","volume":"2","author":"J.W. Klop","year":"1992","unstructured":"J.W. Klop. Term Rewriting Systems. In Handbook of Logic in Computer Science, volume 2, chapter 1, pages 1\u2013116, 1992.","journal-title":"Handbook of Logic in Computer Science"},{"key":"2_CR19","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/0304-3975(86)90109-X","volume":"44","author":"D. Leivant","year":"1986","unstructured":"D. Leivant. Typing and computational properties of lambda expressions. Theoretical Computer Science, 44:51\u201368, 1986.","journal-title":"Theoretical Computer Science"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"F. Pfenning. Partial Polymorphic Type Inference and Higher-Order Unification. In LISP and Functional Programming Languages '88, pages 153\u2013163, 1988.","DOI":"10.1145\/62678.62697"},{"issue":"2","key":"2_CR21","doi-asserted-by":"crossref","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W.W. Tait","year":"1967","unstructured":"W.W. Tait. Intensional interpretation of functional of finite type I. Journal of Symbolic Logic, 32(2):198\u2013223, 1967.","journal-title":"Journal of Symbolic Logic"},{"key":"2_CR22","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/0304-3975(89)90139-4","volume":"65","author":"S.R. Thatte","year":"1989","unstructured":"S.R. Thatte. Full Abstraction and Limiting Completeness in Equational Languages. Theoretical Computer Science, 65:85\u2013119, 1989.","journal-title":"Theoretical Computer Science"},{"key":"2_CR23","doi-asserted-by":"crossref","first-page":"488","DOI":"10.1137\/0205036","volume":"5","author":"C.P. Wadsworth","year":"1976","unstructured":"C.P. Wadsworth. The relation between computational and denotational properties for Scott's D\u221e-models of the lambda-calculus. SIAM J. Comput., 5:488\u2013521, 1976.","journal-title":"SIAM J. Comput."}],"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-61254-8_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:14:49Z","timestamp":1742598889000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61254-8_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540612544","9783540683896"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-61254-8_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}