{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T02:02:34Z","timestamp":1778292154354,"version":"3.51.4"},"publisher-location":"Berlin\/Heidelberg","reference-count":23,"publisher":"Springer-Verlag","isbn-type":[{"value":"3540565175","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0037098","type":"book-chapter","created":{"date-parts":[[2006,1,25]],"date-time":"2006-01-25T15:21:36Z","timestamp":1138202496000},"page":"60-74","source":"Crossref","is-referenced-by-count":10,"title":["Combining first and higher order rewrite systems with type assignment systems"],"prefix":"10.1007","author":[{"given":"Franco","family":"Barbanera","sequence":"first","affiliation":[]},{"given":"Maribel","family":"Fern\u00e1ndez","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"S. van Bakel, S. Smetsers, and S. Brock. Type assignment in left linear applicative term rewriting systems. In Proc. of CAAP'92. Colloquium on Trees in Algebra and Programming, Rennes, France, 1992, 1992.","DOI":"10.1007\/3-540-55251-0_17"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"F. Barbanera. Adding algebraic rewriting to the calculus of constructions: Strong normalization preserved. In Proc. of the 2nd Int. Workshop on Conditional and Typed Rewriting, 1990.","DOI":"10.1007\/3-540-54317-1_96"},{"key":"5_CR3","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1142\/S0129054190000138","volume":"1","author":"F. Barbanera","year":"1990","unstructured":"F. Barbanera. Combining term rewriting and type assignment systems. International Journal of Foundations of Computer Science, 1:165\u2013184, 1990.","journal-title":"International Journal of Foundations of Computer Science"},{"issue":"4","key":"5_CR4","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 \u03bb-model and the completeness of type assignment. Journal of Symbolic Logic, 48(4):931\u2013940, 1983.","journal-title":"Journal of Symbolic Logic"},{"key":"5_CR5","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, 2nd ed., 1984.","edition":"2nd ed."},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Val Breazu-Tannen. Combining algebra and higher-order types. In Proc. 3rd IEEE Symp. Logic in Computer Science, Edinburgh, July 1988.","DOI":"10.1109\/LICS.1988.5103"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Val Breazu-Tannen and Jean Gallier. Polymorphic rewriting conserves algebraic strong normalization. Theoretical Computer Science, 1990. to appear.","DOI":"10.1007\/BFb0035757"},{"key":"5_CR8","unstructured":"F. Cardone and M. Coppo. Two extensions of Curry's type inference system. In P. Odifreddi, editor, Logic and Computer Sciennce. Academic Press, 1990."},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 243\u2013309. North-Holland, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Daniel J. Dougherty. Adding algebraic rewriting to the untyped lambda calculus. In Proc. 4th Rewriting Techniques and Applications, Como, LNCS 488, 1991.","DOI":"10.1007\/3-540-53904-2_84"},{"key":"5_CR11","unstructured":"J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989."},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF. Lecture Notes in Computer Science, 78, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"5_CR13","unstructured":"R. Hindley. Types with intersection, an introduction. Formal aspects of Computing, 1990."},{"key":"5_CR14","unstructured":"R. Hindley and J. Seldin. Introduction to Combinators and \u03bb-calculus. Cambridge University Press, 1986."},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Jean-Pierre Jouannaud and Mitsuhiro Okada. Executable higher-order algebraic specification languages. In Proc. 6th IEEE Symp. Logic in Computer Science, Amsterdam, pages 350\u2013361, 1991.","DOI":"10.1109\/LICS.1991.151659"},{"key":"5_CR16","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, June 1987.","journal-title":"EATCS Bulletin"},{"key":"5_CR17","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"},{"issue":"2","key":"5_CR18","doi-asserted-by":"crossref","first-page":"223","DOI":"10.2307\/1968867","volume":"43","author":"M. H. A. Newman","year":"1942","unstructured":"M. H. A. Newman. On theories with a combinatorial definition of \u2018equivalence'. Ann. Math., 43(2):223\u2013243,1942.","journal-title":"Ann. Math."},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"T. Nipkow. Higher order critical pairs. In Proc. IEEE Symp. on Logic in Comp. Science, Amsterdam, 1991.","DOI":"10.1109\/LICS.1991.151658"},{"key":"5_CR20","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 Proc. ISSAC 89, Portland, Oregon, 1989.","DOI":"10.1145\/74540.74582"},{"key":"5_CR21","unstructured":"G. Pottinger. A type assignment for the strongly normalizable \u03bb-terms. In To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, pages 561\u2013578. Academic Press, 1980."},{"key":"5_CR22","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1016\/0020-0190(87)90122-0","volume":"25","author":"Y. Toyama","year":"1987","unstructured":"Y. Toyama. Counterexamples to termination for the direct sum of term rewriting systems. Information Processing Letters, 25:141\u2013143, April 1987.","journal-title":"Information Processing Letters"},{"key":"5_CR23","series-title":"LNCS 201","volume-title":"Functional Programming Languages and Computer Architecture","author":"D. A. Turner","year":"1985","unstructured":"D. A. Turner. Miranda: A non-strict functional language with polymorphic types. In Functional Programming Languages and Computer Architecture, Nancy, LNCS 201. Springer-Verlag, September 1985."}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0037098.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T11:51:43Z","timestamp":1736250703000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0037098"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540565175"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/bfb0037098","relation":{},"subject":[]}}