{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:46Z","timestamp":1761611206273,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540415176"},{"type":"electronic","value":"9783540445579"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44557-9_3","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T03:04:24Z","timestamp":1180667064000},"page":"41-60","source":"Crossref","is-referenced-by-count":2,"title":["Polymorphic Intersection Type Assignment for Rewrite Systems with Abstraction and \u03b2-Rule"],"prefix":"10.1007","author":[{"given":"Steffen","family":"van Bakel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Franco","family":"Barbanera","sequence":"additional","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":[[2002,6,11]]},"reference":[{"issue":"1","key":"3_CR1","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. TCS, 102(1):135\u2013163, 1992.","journal-title":"TCS"},{"issue":"6","key":"3_CR2","doi-asserted-by":"publisher","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"},{"issue":"2","key":"3_CR3","doi-asserted-by":"publisher","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. TCS, 151(2):385\u2013435, 1995.","journal-title":"TCS"},{"issue":"26","key":"3_CR4","doi-asserted-by":"crossref","first-page":"141","DOI":"10.3233\/FI-1996-26204","volume":"2","author":"S. Bakel van","year":"1996","unstructured":"S. van Bakel. Rank 2 Intersection TypeAssignment in Term Rewriting Systems. Fundamenta Informaticae, 2(26):141\u2013166, 1996.","journal-title":"Fundamenta Informaticae"},{"key":"3_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1007\/3-540-61055-3_50","volume-title":"ESOP\u201996","author":"S. Bakel van","year":"1996","unstructured":"S. van Bakel, F. Barbanera, and M. Fern\u00e1ndez. Rewrite Systems with Abstraction and \u03b2-rule: Types, Approximants and Normalization. In ESOP\u201996, LNCS1058, pages 387\u2013403. Springer-Verlag, 1996."},{"issue":"2","key":"3_CR6","first-page":"73","volume":"133","author":"S. Bakel van","year":"1997","unstructured":"S. van Bakel and M. Fern\u00e1ndez. Normalization Results for Typeable Rewrite Systems. I&C 133(2):73\u2013116, 1997.","journal-title":"Normalization Results for Typeable Rewrite Systems"},{"key":"3_CR7","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/S0304-3975(96)80706-7","volume":"170","author":"F. Barbanera","year":"1996","unstructured":"F. Barbanera and M. Fern\u00e1ndez. Intersection Type Assignment Systems with Higher-Order Algebraic Rewriting. TCS 170:173\u2013207, 1996.","journal-title":"TCS"},{"key":"3_CR8","unstructured":"F. Barbanera, M. Fern\u00e1ndez, and H. Geuvers. Modularity of Strong Normalization and Confluence in the Algebraic \u03bb-cube. In LICS\u2019 94, 1994."},{"key":"3_CR9","unstructured":"H. Barendregt. The Lambda Calculus: its Syntax and Semantics. North-Holland, Amsterdam, revised edition, 1984."},{"issue":"4","key":"3_CR10","doi-asserted-by":"publisher","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. J. of Symbolic Logic, 48(4):931\u2013940, 1983.","journal-title":"J. of Symbolic Logic"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"V. Breazu-Tannen. Combining algebra and higher-order types. In LICS\u2019 88, 1988.","DOI":"10.1109\/LICS.1988.5103"},{"issue":"1","key":"3_CR12","doi-asserted-by":"publisher","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. TCS 83(1):3\u201328, 1991.","journal-title":"TCS"},{"key":"3_CR13","first-page":"3","volume":"82","author":"V. Breazu-Tannen","year":"1992","unstructured":"V. Breazu-Tannen and J. Gallier. Polymorphic rewriting conserves algebraic confluence. I&C 82:3\u201328, 1992.","journal-title":"Polymorphic rewriting conserves algebraic confluence"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"A. Bucciarelli, S. De Lorenzis, A. Piperno, I. Salvo. Some Computational Properties of Intersection Types (Extended Abstract). In LICS\u2019 99, pages 109\u2013118, 1999.","DOI":"10.1109\/LICS.1999.782598"},{"key":"3_CR15","unstructured":"L.M.M. Damas. Type Assignment in Programming Languages. PhD Thesis, University of Edinburgh, 1984."},{"key":"3_CR16","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":"3_CR17","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/0890-5401(92)90064-M","volume":"101","author":"D. J. Dougherty","year":"1992","unstructured":"D. J. Dougherty. Adding algebraic rewriting to the untyped lambda calculus. Information and Computation, 101, 251\u2013267 (1992).","journal-title":"Information and Computation"},{"key":"3_CR18","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1017\/S0960129598002679","volume":"8","author":"M. Fern\u00e1ndez","year":"1998","unstructured":"M Fern\u00e1ndez. Type Assignment and Termination of Interaction Nets. Mathematical Structures in Computer Science, 8:593\u2013636, 1998.","journal-title":"Mathematical Structures in Computer Science"},{"key":"3_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/BFb0020328","volume-title":"Modular termination of term rewriting systems revisited","author":"M. Fern\u00e1ndez","year":"1994","unstructured":"M. Fern\u00e1ndez and J.P. Jouannaud. Modular termination of term rewriting systems revisited. In LNCS 906, pages 255\u2013272. Springer-Verlag, 1994."},{"key":"3_CR20","unstructured":"J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989."},{"key":"3_CR21","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/0304-3975(86)90044-7","volume":"45","author":"J.Y. Girard","year":"1986","unstructured":"J.Y. Girard. The System F of Variable Types, Fifteen years later. TCS 45:159\u2013192, 1986.","journal-title":"TCS"},{"key":"3_CR22","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/0304-3975(92)90070-V","volume":"95","author":"B. Jacobs","year":"1992","unstructured":"B. Jacobs, I. Margaria, and M. Zacchi. Filter models with polymorphic types. TCS 95:143\u2013158, 1992.","journal-title":"TCS"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"T. Jim. What are principal typings and what are they good for? In Proc. POPL\u201996, ACM Symposium on Principles of Programming Language, 1996.","DOI":"10.1145\/237721.237728"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"J.P. Jouannaud and M. Okada. Executable higher-order algebraic specification languages. In LICS\u2019 91, pages 350\u2013361, 1991.","DOI":"10.1109\/LICS.1991.151659"},{"issue":"2","key":"3_CR25","first-page":"228","volume":"98","author":"A.J. Kfoury","year":"1992","unstructured":"A.J. Kfoury and J. Tiuryn. Type reconstruction in finite-rank fragments of the second-order \u03bb-calculus. I&C 98(2):228\u2013257, 1992.","journal-title":"Type reconstruction in finite-rank fragments of the second-order \u03bb-calculus"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"A.J. Kfoury and J.B. Wells. A Direct Algorithm for Type Inference in the Rank-2 Fragment of the Second-Order \u03bb-Calculus. In LFP\u201994, 1994.","DOI":"10.1145\/182409.182456"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"A.J. Kfoury and J.B. Wells. Principality and decidable type inference for finite-rank intersection types. In Proc. 26th ACM Symp. Principles of Prog. Languages, POPL\u2019 99, pages 161\u2013174, 1999.","DOI":"10.1145\/292540.292556"},{"key":"3_CR28","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":"3_CR29","doi-asserted-by":"crossref","unstructured":"J. Launchbury and S.L. Peyton Jones. Lazy functional state threads. In Proc. ACM SIGPLAN\u201994 Conference on Programming Language Design and Implementation, 1994.","DOI":"10.1145\/178243.178246"},{"issue":"3","key":"3_CR30","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1093\/logcom\/5.3.367","volume":"5","author":"I. Margaria","year":"1995","unstructured":"I. Margaria and M. Zacchi. Principal Typing in a \u2200\u2229-Discipline. Logic and Computation, 5(3):367\u2013381, 1995.","journal-title":"Logic and Computation"},{"key":"3_CR31","doi-asserted-by":"publisher","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\u2019. Ann. Math., 43:223\u2013243, 1942.","journal-title":"Ann. Math."},{"key":"3_CR32","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1007\/3-540-54152-7_66","volume-title":"PARLE\u2019 91","author":"E.G.J.M.H. N\u00f6cker","year":"1991","unstructured":"E.G.J.M.H. N\u00f6cker, J.E.W. Smetsers, M.C.J.D. van Eekelen, and M.J. Plasmeijer. Concurrent Clean. In PARLE\u2019 91, LNCS 506-II, pages 202\u2013219. Springer-Verlag, 1991."},{"issue":"1","key":"3_CR33","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"J.A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23\u201341, 1965.","journal-title":"Journal of the ACM"},{"key":"3_CR34","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1016\/0304-3975(83)90069-5","volume":"28","author":"S. Rocca Della","year":"1984","unstructured":"S.Ronchi Della Rocca and B. Venneri. Principal type schemes for an extended type theory. TCS 28:151\u2013169, 1984.","journal-title":"TCS"},{"key":"3_CR35","first-page":"206","volume":"117","author":"H. Yokohuchi","year":"1995","unstructured":"H. Yokohuchi. Embedding a Second-Order Type System into an Intersection Type System. I&C 117:206\u2013220, 1995.","journal-title":"Embedding a Second-Order Type System into an Intersection Type System"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44557-9_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T21:01:15Z","timestamp":1737061275000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44557-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540415176","9783540445579"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/3-540-44557-9_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}