{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,12]],"date-time":"2026-10-12T22:47:51Z","timestamp":1791845271807,"version":"4.3.4"},"reference-count":27,"publisher":"Duke University Press","issue":"1","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Notre Dame J. Formal Logic"],"published-print":{"date-parts":[[2004,1,1]]},"abstract":"<jats:p>This paper defines reduction on derivations (cut-elimination) in the Strict Intersection Type Assignment System of an earlier paper and shows a strong normalization result for this reduction. Using this result, new proofs are given for the approximation theorem and the characterization of normalizability of terms using intersection types.<\/jats:p>","DOI":"10.1305\/ndjfl\/1094155278","type":"journal-article","created":{"date-parts":[[2004,11,2]],"date-time":"2004-11-02T09:32:23Z","timestamp":1099387943000},"page":"35-63","source":"Crossref","is-referenced-by-count":11,"title":["Cut-Elimination in the Strict Intersection Type Assignment System is Strongly Normalizing"],"prefix":"10.1215","volume":"45","author":[{"given":"Steffen","family":"van Bakel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"73","reference":[{"key":"1","unstructured":"[1] Barendregt, H. P., <i>The Lambda Calculus. Its Syntax and Semantics<\/i>, revised edition, vol. 103 of <i>Studies in Logic and the Foundations of Mathematics<\/i>, North-Holland Publishing Co., Amsterdam, 1984."},{"key":"2","doi-asserted-by":"crossref","unstructured":"[2] Barendregt, H., M. Coppo, and M. Dezani-Ciancaglini, \"A filter lambda model and the completeness of type assignment\", <i>The Journal of Symbolic Logic<\/i>, vol. 48 (1983), pp. 931--40.","DOI":"10.2307\/2273659"},{"key":"3","doi-asserted-by":"crossref","unstructured":"[3] Coppo, M., and M. Dezani-Ciancaglini, \"An extension of the basic functionality theory for the $\\lambda $\"-calculus, <i>Notre Dame Journal of Formal Logic<\/i>, vol. 21 (1980), pp. 685--93.","DOI":"10.1305\/ndjfl\/1093883253"},{"key":"5","doi-asserted-by":"crossref","unstructured":"[5] Curry, H. B., \"Functionality in combinatory logic\", <i>Proceedings of the National Academy of Science USA<\/i>, vol. 20 (1934), pp. 584--90.","DOI":"10.1073\/pnas.20.11.584"},{"key":"6","unstructured":"[6] Curry, H. B., and R. Feys, <i>Combinatory Logic. Vol. I<\/i>, Studies in Logic and the Foundations of Mathematics, North-Holland Publishing Co., Amsterdam, 1958."},{"key":"7","doi-asserted-by":"publisher","unstructured":"[7] Dezani-Ciancaglini, M., F. Honsell, and Y. Motohama, \"Approximation theorems for intersection type systems. Type and set theoretical foundations of computation\", <i>Journal of Logic and Computation<\/i>, vol. 11 (2001), pp. 395--417.","DOI":"10.1093\/logcom\/11.3.395"},{"key":"8","doi-asserted-by":"publisher","unstructured":"[8] Dezani-Ciancaglini, M., and I. Margaria, \"A characterization of $F$\"-complete type assignments, <i>Theoretical Computer Science<\/i>, vol. 45 (1986), pp. 121--57.","DOI":"10.1016\/0304-3975(86)90043-5"},{"key":"9","doi-asserted-by":"publisher","unstructured":"[9] Dezani-Ciancaglini, M., R. K. Meyer, and Y. Motohama, \"The semantics of entailment omega\", <i>Notre Dame Journal of Formal Logic<\/i>, vol. 43 (2003), pp. 129--45.","DOI":"10.1305\/ndjfl\/1074290712"},{"key":"10","doi-asserted-by":"crossref","unstructured":"[10] Dougherty, D., and P. Lescanne, \"Reductions, intersection types, and explicit substitutions\", pp. 121--35 in <i>Typed Lambda Calculi and Applications (Krak\u00f3<\/i>w, 2001), vol. 2044 of <i>Lecture Notes in Computer Science<\/i>, Springer, Berlin, 2001.","DOI":"10.1007\/3-540-45413-6_13"},{"key":"11","doi-asserted-by":"publisher","unstructured":"[11] Ghilezan, S., \"Strong normalization and typability with intersection types\", <i>Notre Dame Journal of Formal Logic<\/i>, vol. 37 (1996), pp. 44--52.","DOI":"10.1305\/ndjfl\/1040067315"},{"key":"12","unstructured":"[12] Girard, J.-Y., P. Taylor, and Y. Lafont, <i>Proofs and Types<\/i>, vol. 7 of <i>Cambridge Tracts in Theoretical Computer Science<\/i>, Cambridge University Press, Cambridge, 1989."},{"key":"13","unstructured":"[13] Krivine, J.-L., <i>Lambda-Calcul. Types et Mod\u00e8les<\/i>, \u00c9tudes et Recherches en Informatique. Masson, Paris, 1990."},{"key":"16","doi-asserted-by":"publisher","unstructured":"[16] Ronchi Della Rocca, S., and B. Venneri, \"Principal type schemes for an extended type theory\", <i>Theoretical Computer Science<\/i>, vol. 28 (1984), pp. 151--69.","DOI":"10.1016\/0304-3975(83)90069-5"},{"key":"17","doi-asserted-by":"publisher","unstructured":"[17] Ronchi Della Rocca, S., \"Principal type scheme and unification for intersection type discipline\", <i>Theoretical Computer Science<\/i>, vol. 59 (1988), pp. 181--209. International Joint Conference on Theory and Practice of Software Development (Pisa, 1987).","DOI":"10.1016\/0304-3975(88)90101-6"},{"key":"18","doi-asserted-by":"publisher","unstructured":"[18] Tait, W. W., \"Intensional interpretations of functionals of finite type. I\", <i>The Journal of Symbolic Logic<\/i>, vol. 32 (1967), pp. 198--212.","DOI":"10.2307\/2271658"},{"key":"19","doi-asserted-by":"publisher","unstructured":"[19] van Bakel, S., \"Complete restrictions of the intersection type discipline\", <i>Theoretical Computer Science<\/i>, vol. 102 (1992), pp. 135--63.","DOI":"10.1016\/0304-3975(92)90297-S"},{"key":"20","doi-asserted-by":"publisher","unstructured":"[20] van Bakel, S., \"Intersection type assignment systems\", <i>Theoretical Computer Science<\/i>, vol. 151 (1995), pp. 385--435. Thirteenth Conference on Foundations of Software Technology and Theoretical Computer Science (Bombay, 1993).","DOI":"10.1016\/0304-3975(95)00073-6"},{"key":"22","doi-asserted-by":"publisher","unstructured":"[22] van Bakel, S., F. Barbanera, M. Dezani-Ciancaglini, and F.-J. de Vries, \"Intersection types for $\\lambda$\"-trees, <i>Theoretical Computer Science<\/i>, vol. 272 (2002), pp. 3--40. Theories of types and proofs (Tokyo, 1997).","DOI":"10.1016\/S0304-3975(00)00346-7"},{"key":"23","doi-asserted-by":"crossref","unstructured":"[23] van Bakel, S., and M. Dezani-Ciancaglini, \"Characterising strong normalisation for explicit substitutions\", pp. 356--70 in <i>LATIN 2002: Theoretical Informatics (Cancun)<\/i>, vol. 2286 of <i>Lecture Notes in Computer Science<\/i>, Springer, Berlin, 2002.","DOI":"10.1007\/3-540-45995-2_33"},{"key":"24","doi-asserted-by":"crossref","unstructured":"[24] van Bakel, S., and M. Fern\u00e1ndez, \"Approximation and normalization results for typeable term rewriting systems\", pp. 17--36 in <i>Higher-order Algebra, Logic, and Term Rewriting (Paderborn, 1995)<\/i>, vol. 1074 of <i>Lecture Notes in Computer Science<\/i>, Springer, Berlin, 1996.","DOI":"10.1007\/3-540-61254-8_17"},{"key":"25","doi-asserted-by":"publisher","unstructured":"[25] van Bakel, S., and M. Fern\u00e1ndez, \"Normalization results for typeable rewrite systems\", <i>Information and Computation<\/i>, vol. 133 (1997), pp. 73--116.","DOI":"10.1006\/inco.1996.2617"},{"key":"26","doi-asserted-by":"publisher","unstructured":"[26] van Bakel, S., and M. Fern\u00e1ndez, \"Normalization, approximation, and semantics for combinator systems\", <i>Theoretical Computer Science<\/i>, vol. 290 (2003), pp. 975--1019.","DOI":"10.1016\/S0304-3975(02)00548-0"},{"key":"27","doi-asserted-by":"publisher","unstructured":"[27] Wadsworth, C. P., \"The relation between computational and denotational properties for Scott's $D\\sb\\infty $\"-models of the lambda-calculus, <i>SIAM Journal of Computing<\/i>, vol. 5 (1976), pp. 488--521.","DOI":"10.1137\/0205036"},{"key":"4","doi-asserted-by":"publisher","unstructured":"[4] Coppo, M., M. Dezani-Ciancaglini, and M. Zacchi, \"Type theories, normal forms, and $D\\sb \\infty$\"-lambda-models, <i>Information and Computation<\/i>, vol. 72 (1987), pp. 85--116.","DOI":"10.1016\/0890-5401(87)90042-3"},{"key":"14","unstructured":"[14] Pottinger, G., \"A type assignment for the strongly normalizable $\\lambda $\"-terms, pp. 561--77 in <i>To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism<\/i>, Academic Press, London, 1980."},{"key":"15","unstructured":"[15] Retor\u00e9, C., \"A note on intersection types\", INRIA Rapport de recherche 2431, INRIA, France, 1994."},{"key":"21","doi-asserted-by":"crossref","unstructured":"[21] van Bakel, S., \"Strongly normalising cut-elimination with strict intersection types (extended abstract)\", <i>Proceedings of Intersection Types and Related Systems (ITRS '02)<\/i>, vol. 70 of <i>Electronic Notes in Theoretical Computer Science<\/i>, Elsevier, Amsterdam, 2003. \\hrefhttp:\/\/www.elsevier.nl\/locate\/entcs\/volume70.htmlhttp:\/\/www.elsevier%.nl\/locate\/entcs\/volume70.html.","DOI":"10.1016\/S1571-0661(04)80488-2"}],"container-title":["Notre Dame Journal of Formal Logic"],"original-title":[],"link":[{"URL":"https:\/\/projecteuclid.org\/journalArticle\/Download?urlid=10.1305\/ndjfl\/1094155278","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,10,12]],"date-time":"2026-10-12T22:06:06Z","timestamp":1791842766000},"score":1,"resource":{"primary":{"URL":"https:\/\/projecteuclid.org\/journals\/notre-dame-journal-of-formal-logic\/volume-45\/issue-1\/Cut-Elimination-in-the-Strict-Intersection-Type-Assignment-System-is\/10.1305\/ndjfl\/1094155278.full"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,1,1]]},"references-count":27,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2004,1,1]]}},"URL":"https:\/\/doi.org\/10.1305\/ndjfl\/1094155278","relation":{},"ISSN":["0029-4527","1939-0726"],"issn-type":[{"value":"0029-4527","type":"print"},{"value":"1939-0726","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,1,1]]}}}