{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T12:17:41Z","timestamp":1790079461364,"version":"4.0.1"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540610557","type":"print"},{"value":"9783540499428","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61055-3_50","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:14:11Z","timestamp":1330290851000},"page":"387-403","source":"Crossref","is-referenced-by-count":2,"title":["Rewrite systems with abstraction and \u03b2-rule: Types, approximants and normalization"],"prefix":"10.1007","author":[{"given":"Steffen","family":"Bakel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Franco","family":"Barbanera","sequence":"additional","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,2]]},"reference":[{"key":"25_CR1","first-page":"543","volume":"789","author":"Z. Ariola","year":"1994","unstructured":"Ariola Z., R. Kennaway, J.W. Klop, R. Sleep and F-J. de Vries. Syntactic definitions of undefined: on defining the undefined. In Proceedings of TACS '94, volume 789 of LNCS, pages 543\u2013554, 1994.","journal-title":"LNCS"},{"key":"25_CR2","doi-asserted-by":"publisher","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":"25_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 Proceedings of TLCA '93, volume 664 of LNCS, pages 29\u201344, 1993.","journal-title":"LNCS"},{"issue":"2","key":"25_CR4","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1016\/0304-3975(95)00073-6","volume":"151","author":"S. Bakel van","year":"1995","unstructured":"S. van Bakel. Intersection Type Assignment Systems. Theoretical Computer Science, 151(2):385\u2013435, 1995.","journal-title":"Theoretical Computer Science"},{"key":"25_CR5","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 Proceedings of HOA '93, volume 816 of LNCS, pages 20\u201339, 1994.","journal-title":"LNCS"},{"key":"25_CR6","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. In Proceedings of RTA '95, volume 914 of LNCS, pages 279\u2013293, 1995.","journal-title":"LNCS"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"S. van Bakel and M. Fern\u00e1ndez. Approximation and Normalization Results for Typeable Rewrite Systems. To appear in Proceedings of HOA '95, Paderborn, Germany, 1995.","DOI":"10.1007\/3-540-59200-8_64"},{"key":"25_CR8","first-page":"60","volume":"664","author":"F. Barbanera","year":"1993","unstructured":"F. Barbanera and M. Fern\u00e1ndez. Combining first and higher order rewrite systems with type assignment systems. In Proceedings of TLCA '93, volume 664 of LNCS, pages 60\u201374, 1993.","journal-title":"LNCS"},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"F. Barbanera, M. Fern\u00e1ndez, and H. Geuvers. Modularity of Strong Normalization and Confluence in the \u03bb-algebraic-cube. In Proceedings of LICS'94, 1994.","DOI":"10.1109\/LICS.1994.316049"},{"key":"25_CR10","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":"25_CR11","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":"25_CR12","doi-asserted-by":"crossref","unstructured":"V. Breazu-Tannen. Combining algebra and higher-order types. In Proceedings of LICS'88, pages 82\u201390, 1988.","DOI":"10.1109\/LICS.1988.5103"},{"issue":"1","key":"25_CR13","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(91)90037-3","volume":"83","author":"V. Breazu-Tannen","year":"1991","unstructured":"V. Breazu-Tannen and J. Gallier. Polymorphic rewriting conserves algebraic strong normalization. Theoretical Computer Science, 83(1):3\u201328, 1991.","journal-title":"Theoretical Computer Science"},{"key":"25_CR14","first-page":"3","volume":"82","author":"V. Breazu-Tannen","year":"1992","unstructured":"V. Breazu-Tannen and J. Gallier. Polymorphic rewriting conserves algebraic confluence. Information and Computation, 82:3\u201328, 1992.","journal-title":"Information and Computation"},{"key":"25_CR15","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":"25_CR16","first-page":"37","volume":"488","author":"D. J. Dougherty","year":"1991","unstructured":"D. J. Dougherty. Adding Algebraic Rewriting to the Untyped Lambda Calculus. In Proceedings of RTA '91, volume 488 of LNCS, pages 37\u201348. 1991.","journal-title":"LNCS"},{"key":"25_CR17","unstructured":"J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989."},{"key":"25_CR18","doi-asserted-by":"crossref","unstructured":"M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF. Lecture Notes in Computer Science, volume 78, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"25_CR19","unstructured":"G. Huet and J.J. L\u00e9vy. Computations in Orthogonal Rewriting Systems. In J.-L. Lassez and G. Plotkin, editors, Computational Logic. Essays in Honour of Alan Robinson. MIT Press, 1991."},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"J.P. Jouannaud and M. Okada. Executable higher-order algebraic specification languages. In Proceedings of LICS'91, pages 350\u2013361, 1991.","DOI":"10.1109\/LICS.1991.151659"},{"key":"25_CR21","first-page":"143","volume":"32","author":"J.W. Klop","year":"1987","unstructured":"J.W. Klop. Term Rewriting Systems: a tutorial. EATCS Bulletin, 32:143\u2013182, 1987.","journal-title":"EATCS Bulletin"},{"key":"25_CR22","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":"25_CR23","doi-asserted-by":"crossref","unstructured":"Mitsuhiro Okada. Strong normalizability for the combined system of the types lambda calculus and an arbitrary convergent term rewrite system. In Proceedings of ISSAC 89, Portland, Oregon, 1989.","DOI":"10.1145\/74540.74582"},{"issue":"2","key":"25_CR24","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 functionals of finite type I. Journal of Symbolic Logic, 32(2):198\u2013223, 1967.","journal-title":"Journal of Symbolic Logic"},{"key":"25_CR25","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":"25_CR26","first-page":"1","volume":"201","author":"D.A. Turner","year":"1985","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, volume 201 of LNCS, pages 1\u201316, 1985.","journal-title":"LNCS"},{"key":"25_CR27","doi-asserted-by":"publisher","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","Programming Languages and Systems \u2014 ESOP '96"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61055-3_50.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:13:08Z","timestamp":1742598788000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61055-3_50"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540610557","9783540499428"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-61055-3_50","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}