{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,30]],"date-time":"2026-09-30T03:03:32Z","timestamp":1790737412800,"version":"4.1.0"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2011,4,1]],"date-time":"2011-04-01T00:00:00Z","timestamp":1301616000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Comput. Surv."],"published-print":{"date-parts":[[2011,4]]},"abstract":"<jats:p>This article will show the usefulness and elegance of strict intersection types for the Lambda Calculus, that are strict in the sense that they are the representatives of equivalence classes of types in the BCD-system [Barendregt et al. 1983]. We will focus on the essential intersection type assignment; this system is almost syntax directed, and we will show that all major properties hold that are known to hold for other intersection systems, like the approximation theorem, the characterization of (head\/strong) normalization, completeness of type assignment using filter semantics, strong normalization for cut-elimination and the principal pair property. In part, the proofs for these properties are new; we will briefly compare the essential system with other existing systems.<\/jats:p>","DOI":"10.1145\/1922649.1922657","type":"journal-article","created":{"date-parts":[[2011,5,3]],"date-time":"2011-05-03T12:48:53Z","timestamp":1304426933000},"page":"1-49","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["Strict intersection types for the Lambda Calculus"],"prefix":"10.1145","volume":"43","author":[{"given":"Steffen Van","family":"Bakel","sequence":"first","affiliation":[{"name":"Imperial College London, London, U.K."}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2011,4,29]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"crossref","unstructured":"Alessi F. Barbanera F. and Dezani-Ciancaglini M. 2003. Intersection types and computational rules. Electro. Notes Theoret. Comput. Sci. 84.  Alessi F. Barbanera F. and Dezani-Ciancaglini M. 2003. Intersection types and computational rules. Electro. Notes Theoret. Comput. Sci. 84.","DOI":"10.1016\/S1571-0661(04)80843-0"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90297-S"},{"key":"e_1_2_2_4_1","volume-title":"Proceedings of 13th Conference on Foundations of Software Technology and Theoretical Computer Science (FST&amp;amp;TCS)","author":"Bakel S.","unstructured":"Bakel , S. van 1993a. Essential intersection type assignment . In Proceedings of 13th Conference on Foundations of Software Technology and Theoretical Computer Science (FST&amp;amp;TCS) . R. Shyamasunda, Ed. Lecture Notes in Computer Science, vol. 761 . Springer-Verlag , 13--23. Bakel, S. van 1993a. Essential intersection type assignment. In Proceedings of 13th Conference on Foundations of Software Technology and Theoretical Computer Science (FST&amp;amp;TCS). R. Shyamasunda, Ed. Lecture Notes in Computer Science, vol. 761. Springer-Verlag, 13--23."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/3.6.643"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00073-6"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/2379532.2379536"},{"key":"e_1_2_2_9_1","volume-title":"Electronic Proceedings of the International Workshop on Types in Programming (TIP)","volume":"75","author":"Bakel S.","year":"2002","unstructured":"Bakel , S. van 2002 . Rank 2 types for term graph rewriting (extended abstract) . In Electronic Proceedings of the International Workshop on Types in Programming (TIP) . Dagstuhl, Germany. Vol. 75 . Bakel, S. van 2002. Rank 2 types for term graph rewriting (extended abstract). In Electronic Proceedings of the International Workshop on Types in Programming (TIP). Dagstuhl, Germany. Vol. 75."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1094155278"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.01.020"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.2617"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00548-0"},{"key":"e_1_2_2_14_1","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"Barendregt H.","unstructured":"Barendregt , H. 1984. The Lambda Calculus: Its Syntax and Semantics . Revised Ed. North-Holland, Amsterdam . Barendregt, H. 1984. The Lambda Calculus: Its Syntax and Semantics. Revised Ed. North-Holland, Amsterdam."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273659"},{"key":"e_1_2_2_16_1","volume-title":"Strictness analysis of lazy functional programs. Tech. rep. 309 Computing Lab","author":"Benton P. N.","unstructured":"Benton , P. N. 1993. Strictness analysis of lazy functional programs. Tech. rep. 309 Computing Lab , University of Cambridge . Benton, P. N. 1993. Strictness analysis of lazy functional programs. Tech. rep. 309 Computing Lab, University of Cambridge."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90019-0"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.2307\/2269326"},{"key":"e_1_2_2_19_1","volume-title":"Proceedings of 6th International Colloquium on Automata, Languages and Programming (ICALP)","author":"Coppo M.","unstructured":"Coppo , M. , Dezani, M. , and Sall &amp;#233;, P. 1979. Functional characterization of some semantic equalities inside &amp;#955;-calculus . In Proceedings of 6th International Colloquium on Automata, Languages and Programming (ICALP) . H. Maurer, Ed., Lecture Notes in Computer Science, vol. 71 , Springer-Verlag , 133--146. Coppo, M., Dezani, M., and Sall&amp;#233;, P. 1979. Functional characterization of some semantic equalities inside &amp;#955;-calculus. In Proceedings of 6th International Colloquium on Automata, Languages and Programming (ICALP). H. Maurer, Ed., Lecture Notes in Computer Science, vol. 71, Springer-Verlag, 133--146."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093883253"},{"key":"e_1_2_2_21_1","unstructured":"Coppo M. Dezani-Ciancaglini M. and Venneri B. 1980. Principal type schemes and &amp;#955;-calculus semantics. In To H.B. Curry Essays in Combinatory Logic Lambda-Calculus and Formalism J. Hindley and J. Seldin Eds. Academic Press New York 535--560.  Coppo M. Dezani-Ciancaglini M. and Venneri B. 1980. Principal type schemes and &amp;#955;-calculus semantics. In To H.B. Curry Essays in Combinatory Logic Lambda-Calculus and Formalism J. Hindley and J. Seldin Eds. Academic Press New York 535--560."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19810270205"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(87)90042-3"},{"key":"e_1_2_2_24_1","unstructured":"Coppo M. and Ferrari A. 1993. Type inference abstract interpretation and strictness analysis. In A Collection of Contributions in Honour of Corrado B&amp;#246;hm M. Dezani-Ciancaglini S. Ronchi Della Rocca and M. Venturini Zilli Eds. Elsevier 113--145.  Coppo M. and Ferrari A. 1993. Type inference abstract interpretation and strictness analysis. In A Collection of Contributions in Honour of Corrado B&amp;#246;hm M. Dezani-Ciancaglini S. Ronchi Della Rocca and M. Venturini Zilli Eds. Elsevier 113--145."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.20.11.584"},{"key":"e_1_2_2_26_1","unstructured":"Curry H. and Feys R. 1958. Combinatory Logic. Vol. 1. North-Holland Amsterdam.  Curry H. and Feys R. 1958. Combinatory Logic. Vol. 1. North-Holland Amsterdam."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/582153.582176"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/646792.704693"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/778559.778560"},{"key":"e_1_2_2_30_1","doi-asserted-by":"crossref","unstructured":"Damiani F.\n       and Giannini P\n  . \n  1994\n  . A decidable intersection type system based on relevance. In Proceedings of the International Symposium on Theoretical Aspects of Computer Software (TACS). M. Hagiya and J. Mitchell Eds. Lecture Notes in Computer Science vol. \n  789 Springer-Verlag 707--725.   Damiani F. and Giannini P. 1994. A decidable intersection type system based on relevance. In Proceedings of the International Symposium on Theoretical Aspects of Computer Software (TACS). M. Hagiya and J. Mitchell Eds. Lecture Notes in Computer Science vol. 789 Springer-Verlag 707--725.","DOI":"10.1007\/3-540-57887-0_122"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/21541.21542"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1074290712"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02483849"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/21541.21543"},{"key":"e_1_2_2_35_1","doi-asserted-by":"crossref","unstructured":"Gunter C. and Scott D. 1990. Semantic domains. In Handbook of Theoretical Computer Science J. van Leeuwen Ed. North-Holland 633--674.   Gunter C. and Scott D. 1990. Semantic domains. In Handbook of Theoretical Computer Science J. van Leeuwen Ed. North-Holland 633--674.","DOI":"10.1016\/B978-0-444-88074-1.50017-2"},{"key":"e_1_2_2_36_1","first-page":"29","article-title":"The principal type scheme of an object in combinatory logic","volume":"146","author":"Hindley J.","year":"1969","unstructured":"Hindley , J. 1969 . The principal type scheme of an object in combinatory logic . Trans. Amer. Math. Soc. 146 , 29 -- 60 . Hindley, J. 1969. The principal type scheme of an object in combinatory logic. Trans. Amer. Math. Soc. 146, 29--60.","journal-title":"Trans. Amer. Math. Soc."},{"key":"e_1_2_2_37_1","series-title":"Lecture Notes in Computer Science","volume-title":"The simple semantics for Coppo-Dezani-Sall&amp;#233","author":"Hindley J.","unstructured":"Hindley , J. 1982. The simple semantics for Coppo-Dezani-Sall&amp;#233 ; type assignment. In Proceedings of the International Symposium on Programming. M. Dezani and U. Montanari, Eds., Lecture Notes in Computer Science , vol. 137 . Springer-Verlag , 212--226. Hindley, J. 1982. The simple semantics for Coppo-Dezani-Sall&amp;#233; type assignment. In Proceedings of the International Symposium on Programming. M. Dezani and U. Montanari, Eds., Lecture Notes in Computer Science, vol. 137. Springer-Verlag, 212--226."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90136-6"},{"key":"e_1_2_2_39_1","volume-title":"Basic Simple Type Theory","author":"Hindley J.","unstructured":"Hindley , J. 1997. Basic Simple Type Theory . Cambridge University Press . Hindley, J. 1997. Basic Simple Type Theory. Cambridge University Press."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19800261902"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/130697.130699"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/5.4.397"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237728"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/317636.317788"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292556"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/567067.567077"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90009-0"},{"key":"e_1_2_2_51_1","unstructured":"Retor&amp;#233; C. 1994. A note on intersection types. INRIA Rapport de recherche 2431 INRIA France.  Retor&amp;#233; C. 1994. A note on intersection types. INRIA Rapport de recherche 2431 INRIA France."},{"key":"e_1_2_2_52_1","volume-title":"The essence of Algol","author":"Reynolds J. C.","unstructured":"Reynolds , J. C. 1981. The essence of Algol . In Algorithmic Languages, J. de Bakker and J. van Vliet, Eds., North-Holland , 345--372. Reynolds, J. C. 1981. The essence of Algol. In Algorithmic Languages, J. de Bakker and J. van Vliet, Eds., North-Holland, 345--372."},{"key":"e_1_2_2_53_1","volume-title":"Preliminary design of the programming language Forsythe. Tech. rep. CMU-CS-88-159","author":"Reynolds J. C.","unstructured":"Reynolds , J. C. 1988. Preliminary design of the programming language Forsythe. Tech. rep. CMU-CS-88-159 , Carnegie Mellon University , Pitssburgh, PA . Reynolds, J. C. 1988. Preliminary design of the programming language Forsythe. Tech. rep. CMU-CS-88-159, Carnegie Mellon University, Pitssburgh, PA."},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90101-6"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90069-5"},{"key":"e_1_2_2_57_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 5th Colloquium on Automata, Languages and Programming. G. Ausiello and C. B&amp;#246;hm, Eds.","author":"Sall P.","unstructured":"Sall &amp;#233;, P. 1978. Une extension de la th&amp;#233;orie des types . In Proceedings of the 5th Colloquium on Automata, Languages and Programming. G. Ausiello and C. B&amp;#246;hm, Eds. , Lecture Notes in Computer Science , vol. 62 , Springer-Verlag , 398--410. Sall&amp;#233;, P. 1978. Une extension de la th&amp;#233;orie des types. In Proceedings of the 5th Colloquium on Automata, Languages and Programming. G. Ausiello and C. B&amp;#246;hm, Eds., Lecture Notes in Computer Science, vol. 62, Springer-Verlag, 398--410."},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.41"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1137\/0205036"},{"key":"e_1_2_2_61_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 29th International Colloquium on Automata, Languages and Programming (ICALP)","author":"Wells J.","unstructured":"Wells , J. 2002. The essence of principal typings . In Proceedings of the 29th International Colloquium on Automata, Languages and Programming (ICALP) . Lecture Notes in Computer Science , vol. 2380 . Springer-Verlag , 913--925. Wells, J. 2002. The essence of principal typings. In Proceedings of the 29th International Colloquium on Automata, Languages and Programming (ICALP). Lecture Notes in Computer Science, vol. 2380. Springer-Verlag, 913--925."}],"container-title":["ACM Computing Surveys"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1922649.1922657","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1922649.1922657","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:26:08Z","timestamp":1750278368000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1922649.1922657"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,4]]},"references-count":57,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2011,4]]}},"alternative-id":["10.1145\/1922649.1922657"],"URL":"https:\/\/doi.org\/10.1145\/1922649.1922657","relation":{},"ISSN":["0360-0300","1557-7341"],"issn-type":[{"value":"0360-0300","type":"print"},{"value":"1557-7341","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,4]]},"assertion":[{"value":"2006-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}