{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:27:29Z","timestamp":1725571649677},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540255932"},{"type":"electronic","value":"9783540320142"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11417170_12","type":"book-chapter","created":{"date-parts":[[2010,12,16]],"date-time":"2010-12-16T19:29:35Z","timestamp":1292527775000},"page":"146-161","source":"Crossref","is-referenced-by-count":4,"title":["Rank-2 Intersection and Polymorphic Recursion"],"prefix":"10.1007","author":[{"given":"Ferruccio","family":"Damiani","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"publisher","first-page":"931","DOI":"10.2307\/2273659","volume":"48","author":"H.P. Barendregt","year":"1983","unstructured":"Barendregt, H.P., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. J.\u00a0of Symbolic Logic\u00a048, 931\u2013940 (1983)","journal-title":"J.\u00a0of Symbolic Logic"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-24725-8_21","volume-title":"Programming Languages and Systems","author":"S. Carlier","year":"2004","unstructured":"Carlier, S., Polakow, J., Wells, J.B., Kfoury, A.J.: System E: Expansion variables for flexible typing with linear and non-linear types and intersection types. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 294\u2013309. Springer, Heidelberg (2004)"},{"issue":"4","key":"12_CR3","doi-asserted-by":"publisher","first-page":"685","DOI":"10.1305\/ndjfl\/1093883253","volume":"21","author":"M. Coppo","year":"1980","unstructured":"Coppo, M., Dezani-Ciancaglini, M.: An extension of basic functional theory for lambda-calculus. Notre Dame Journal of Formal Logic\u00a021(4), 685\u2013693 (1980)","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"12_CR4","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1145\/263699.263744","volume-title":"POPL 1997","author":"P. Cousot","year":"1997","unstructured":"Cousot, P.: Types as Abstract Interpretations. In: POPL 1997, pp. 316\u2013331. ACM, New York (1997)"},{"key":"12_CR5","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1145\/582153.582176","volume-title":"POPL 1982","author":"L.M.M. Damas","year":"1982","unstructured":"Damas, L.M.M., Milner, R.: Principal type schemas for functional programs. In: POPL 1982, pp. 207\u2013212. ACM, New York (1982)"},{"issue":"4","key":"12_CR6","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1145\/778559.778560","volume":"25","author":"F. Damiani","year":"2003","unstructured":"Damiani, F.: Rank 2 intersection types for local definitions and conditional expressions. ACM Trans.\u00a0Prog.\u00a0Lang.\u00a0Syst.\u00a025(4), 401\u2013451 (2003)","journal-title":"ACM Trans.\u00a0Prog.\u00a0Lang.\u00a0Syst."},{"key":"12_CR7","unstructured":"Girard, J.Y.: Interpretation fonctionelle et elimination des coupures dans l\u2019aritmetique d\u2019ordre superieur. PhD thesis, Universit\u00e9 Paris VII (1972)"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/3-540-36384-X_13","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R. Gori","year":"2002","unstructured":"Gori, R., Levi, G.: Properties of a type abstract interpreter. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 132\u2013145. Springer, Heidelberg (2002)"},{"key":"12_CR9","unstructured":"Hallett, J.J., Kfoury, A.J.: Programming examples needing polymorphic recursion. In: ITRS 2004 (workshop affiliated to LICS 2004), ENTCS. Elsevier, Amsterdam (2004) (to appear)"},{"issue":"2","key":"12_CR10","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/169701.169692","volume":"15","author":"F. Henglein","year":"1993","unstructured":"Henglein, F.: Type inference with polymorphic recursion. ACM Trans.\u00a0Prog.\u00a0Lang.\u00a0Syst.\u00a015(2), 253\u2013289 (1993)","journal-title":"ACM Trans.\u00a0Prog.\u00a0Lang.\u00a0Syst."},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Hindley, R.: Basic Simple Type Theory. In: Cambridge Tracts in Theoretical Computer Science, vol.\u00a042. Cambridge University Press, London (1997)","DOI":"10.1017\/CBO9780511608865"},{"key":"12_CR12","unstructured":"Jim, T.: Rank 2 type systems and recursive definitions. Technical Report MIT\/LCS\/TM-531, LCS, Massachusetts Institute of Technology (1995)"},{"key":"12_CR13","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1145\/237721.237728","volume-title":"POPL 1996","author":"T. Jim","year":"1996","unstructured":"Jim, T.: What are principal typings and what are they good for? In: POPL 1996, pp. 42\u201353. ACM, New York (1996)"},{"key":"12_CR14","unstructured":"Jim, T.: A polar type system. In: ICALP Workshops, Proceedings in Informatics, vol.\u00a08, pp. 323\u2013338. Carleton-Scientific, Ottawa (2000)"},{"issue":"2","key":"12_CR15","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1145\/169701.169687","volume":"15","author":"A.J. Kfoury","year":"1993","unstructured":"Kfoury, A.J., Tiuryn, J., Urzyczyn, P.: Type reconstruction in the presence of polymorphic recursion. ACM Trans.\u00a0Prog.\u00a0Lang.\u00a0Syst.\u00a015(2), 290\u2013311 (1993)","journal-title":"ACM Trans.\u00a0Prog.\u00a0Lang.\u00a0Syst."},{"key":"12_CR16","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1145\/567067.567077","volume-title":"POPL 1983","author":"D. Leivant","year":"1983","unstructured":"Leivant, D.: Polymorphic Type Inference. In: POPL 1983, pp. 88\u201398. ACM, New York (1983)"},{"key":"12_CR17","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1145\/567067.567092","volume-title":"POPL 1983","author":"L. Meertens","year":"1983","unstructured":"Meertens, L.: Incremental polymorphic type checking in B. In: POPL 1983, pp. 265\u2013275. ACM, New York (1983)"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/3-540-12925-1_41","volume-title":"International Symposium on Programming","author":"A. Mycroft","year":"1984","unstructured":"Mycroft, A.: Polymorphic Type Schemes and Recursive Definitions. In: Paul, M., Robinet, B. (eds.) Programming 1984. LNCS, vol.\u00a0167, pp. 217\u2013228. Springer, Heidelberg (1984)"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"408","DOI":"10.1007\/3-540-06859-7_148","volume-title":"Programming Symposium","author":"J.C. Reynolds","year":"1974","unstructured":"Reynolds, J.C.: Towards a Theory of Type Structure. In: Robinet, B. (ed.) Programming Symposium. LNCS, vol.\u00a019, pp. 408\u2013425. Springer, Heidelberg (1974)"},{"key":"12_CR20","unstructured":"van Bakel, S.: Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting Systems. PhD thesis, Katholieke Universiteit Nijmegen (1993)"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"van Bakel, S.: Rank 2 types for term graph rewriting. In: TIP 2002. ENTCS, vol.\u00a075. Elsevier, Amsterdam (2003)","DOI":"10.1016\/S1571-0661(04)80776-X"},{"key":"12_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"913","DOI":"10.1007\/3-540-45465-9_78","volume-title":"Automata, Languages and Programming","author":"J.B. Wells","year":"2002","unstructured":"Wells, J.B.: The essence of principal typings. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol.\u00a02380, pp. 913\u2013925. Springer, Heidelberg (2002)"},{"key":"12_CR23","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1006\/inco.1995.1040","volume":"117","author":"H. Yokouchi","year":"1995","unstructured":"Yokouchi, H.: Embedding a Second-Order Type System into an Intersection Type System. Information and Computation\u00a0117, 206\u2013220 (1995)","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11417170_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:03:46Z","timestamp":1619507026000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11417170_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540255932","9783540320142"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/11417170_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}