{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:22:11Z","timestamp":1751660531475,"version":"3.40.3"},"publisher-location":"Cham","reference-count":47,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031177149"},{"type":"electronic","value":"9783031177156"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-17715-6_29","type":"book-chapter","created":{"date-parts":[[2022,10,2]],"date-time":"2022-10-02T09:02:27Z","timestamp":1664701347000},"page":"462-480","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Type Inference for\u00a0Rank-2 Intersection Types Using Set Unification"],"prefix":"10.1007","author":[{"given":"Pedro","family":"\u00c2ngelo","sequence":"first","affiliation":[]},{"given":"M\u00e1rio","family":"Florido","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,10,3]]},"reference":[{"key":"29_CR1","doi-asserted-by":"crossref","unstructured":"Accattoli, B., Graham-Lengrand, S., Kesner, D.: Tight typings and split bounds. In: Proceeding ACM Programming Language, vol. 2(ICFP), pp. 94:1\u201394:30 (2018)","DOI":"10.1145\/3236789"},{"key":"29_CR2","unstructured":"Alves, S., Kesner, D., Ventura, D.: A quantitative understanding of pattern matching. In: 25th International Conference on Types for Proofs and Programs, TYPES 2019, 11\u201314 June 2019, Oslo, Norway. LIPIcs, vol. 175, pp. 3:1\u20133:36. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019)"},{"key":"29_CR3","doi-asserted-by":"publisher","unstructured":"\u00c2ngelo, P., Florido, M.: Type inference for rank 2 gradual intersection types. In: Bowman, W.J., Garcia, R. (eds.) Trends in Functional Programming, pp. 84\u2013120. Springer International Publishing, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-47147-7_5","DOI":"10.1007\/978-3-030-47147-7_5"},{"key":"29_CR4","doi-asserted-by":"crossref","unstructured":"\u00c2ngelo, P., Florido, M.: Type inference for rank-2 intersection types using set unification. Technical report, Faculdade de Ci\u00eancias & LIACC, Universidade do Porto (2022). https:\/\/raw.githubusercontent.com\/pedroangelo\/papers\/master\/angelo2022type_complete.pdf","DOI":"10.1007\/978-3-031-17715-6_29"},{"key":"29_CR5","doi-asserted-by":"crossref","unstructured":"Barendregt, H.P., Dekkers, W., Statman, R.: Lambda Calculus with Types. Perspectives in logic, Cambridge University Press (2013)","DOI":"10.1017\/CBO9781139032636"},{"issue":"4","key":"29_CR6","doi-asserted-by":"publisher","first-page":"931","DOI":"10.2307\/2273659","volume":"48","author":"H Barendregt","year":"1983","unstructured":"Barendregt, H., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. J. Symb. Log. 48(4), 931\u2013940 (1983). https:\/\/doi.org\/10.2307\/2273659","journal-title":"J. Symb. Log."},{"key":"29_CR7","unstructured":"Bettini, L., Bono, V., Dezani-Ciancaglini, M., Giannini, P., Venneri, B.: Java & lambda: a featherweight story. Log. Methods Comput. Sci. 14(3) (2018)"},{"key":"29_CR8","doi-asserted-by":"publisher","unstructured":"Boudol, G., Zimmer, P.: On type inference in the intersection type discipline. Electron. Notes Theor. Comput. Sci. 136, 23\u201342 (2005). https:\/\/doi.org\/10.1016\/j.entcs.2005.06.016, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S1571066105050589. Proceedings of the Third International Workshop on Intersection Types and Related Systems (ITRS 2004)","DOI":"10.1016\/j.entcs.2005.06.016"},{"issue":"4","key":"29_CR9","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1093\/jigpal\/jzx018","volume":"25","author":"A Bucciarelli","year":"2017","unstructured":"Bucciarelli, A., Kesner, D., Ventura, D.: Non-idempotent intersection types for the Lambda-Calculus. Logic J. IGPL 25(4), 431\u2013464 (2017). https:\/\/doi.org\/10.1093\/jigpal\/jzx018","journal-title":"Logic J. IGPL"},{"key":"29_CR10","doi-asserted-by":"publisher","unstructured":"Carlier, S., Wells, J.B.: Type inference with expansion variables and intersection types in system e and an exact correspondence with $$\\beta $$-reduction. In: Proceedings of the 6th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pp. 132\u2013143. PPDP 2004. Association for Computing Machinery, New York, NY, USA (2004). https:\/\/doi.org\/10.1145\/1013963.1013980","DOI":"10.1145\/1013963.1013980"},{"key":"29_CR11","doi-asserted-by":"publisher","unstructured":"Castagna, G., Lanvin, V.: Gradual typing with union and intersection types. Proc. ACM Program. Lang. 1(ICFP), 1, 41:1\u201341:28 (2017). https:\/\/doi.org\/10.1145\/3110285","DOI":"10.1145\/3110285"},{"key":"29_CR12","doi-asserted-by":"publisher","unstructured":"Castagna, G., Lanvin, V., Petrucciani, T., Siek, J.G.: Gradual typing: a new perspective. Proc. ACM Program. Lang. 3(POPL), 16:1\u201316:32 (2019). https:\/\/doi.org\/10.1145\/3290329","DOI":"10.1145\/3290329"},{"issue":"4","key":"29_CR13","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 the basic functionality theory for the $$\\lambda $$-calculus. Notre Dame J. Formal Logic 21(4), 685\u2013693 (1980). https:\/\/doi.org\/10.1305\/ndjfl\/1093883253","journal-title":"Notre Dame J. Formal Logic"},{"issue":"1","key":"29_CR14","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1006\/inco.1995.1141","volume":"122","author":"M Coppo","year":"1995","unstructured":"Coppo, M., Giannini, P.: Principal types and unification for simple intersection type systems. Inf. Comput. 122(1), 70\u201396 (1995). https:\/\/doi.org\/10.1006\/inco.1995.1141","journal-title":"Inf. Comput."},{"key":"29_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/BFb0022505","volume-title":"Mathematical Foundations of Computer Science 1980","author":"M Coppo","year":"1980","unstructured":"Coppo, M.: An extended polymorphic type system for applicative languages. In: Dembi\u0144ski, P. (ed.) MFCS 1980. LNCS, vol. 88, pp. 194\u2013204. Springer, Heidelberg (1980). https:\/\/doi.org\/10.1007\/BFb0022505"},{"issue":"11","key":"29_CR16","doi-asserted-by":"publisher","first-page":"584","DOI":"10.1073\/pnas.20.11.584","volume":"20","author":"HB Curry","year":"1934","unstructured":"Curry, H.B.: Functionality in combinatory logic. Proc. Nat. Acad. Sci. 20(11), 584\u2013590 (1934). https:\/\/doi.org\/10.1073\/pnas.20.11.584","journal-title":"Proc. Nat. Acad. Sci."},{"key":"29_CR17","doi-asserted-by":"publisher","unstructured":"Damas, L., Milner, R.: Principal type-schemes for functional programs. In: Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 207\u2013212. POPL 1982. ACM, New York, NY, USA (1982). https:\/\/doi.org\/10.1145\/582153.582176","DOI":"10.1145\/582153.582176"},{"key":"29_CR18","doi-asserted-by":"publisher","unstructured":"Damiani, F.: Rank 2 intersection types for modules. In: Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declaritive Programming, pp. 67\u201378. PPDP 2003. Association for Computing Machinery, New York, NY, USA (2003). https:\/\/doi.org\/10.1145\/888251.888259","DOI":"10.1145\/888251.888259"},{"key":"29_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"707","DOI":"10.1007\/3-540-57887-0_122","volume-title":"Theoretical Aspects of Computer Software","author":"F Damiani","year":"1994","unstructured":"Damiani, F., Giannini, P.: A decidable intersection type system based on relevance. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 707\u2013725. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-57887-0_122"},{"key":"29_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0743-1066(95)00147-6","volume":"28","author":"A Dovier","year":"1996","unstructured":"Dovier, A., Omodeo, E., Pontelli, E., Rossi, G.: A language for programming in logic with finite sets. J. Log. Program. 28, 1\u201344 (1996)","journal-title":"J. Log. Program."},{"issue":"6","key":"29_CR21","doi-asserted-by":"publisher","first-page":"645","DOI":"10.1017\/S1471068406002730","volume":"6","author":"A Dovier","year":"2006","unstructured":"Dovier, A., Pontelli, E., Rossi, G.: Set unification. Theory Pract. Logic Program. 6(6), 645\u2013701 (2006). https:\/\/doi.org\/10.1017\/S1471068406002730","journal-title":"Theory Pract. Logic Program."},{"key":"29_CR22","unstructured":"Dudenhefner, A., Martens, M., Rehof, J.: The algebraic intersection type unification problem. Log. Meth. Comput. Sci. 13 (2017)"},{"key":"29_CR23","doi-asserted-by":"publisher","unstructured":"Dunfield, J.: Elaborating intersection and union types. In: Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, pp. 17\u201328. ICFP 2012. Association for Computing Machinery, New York, NY, USA (2012). https:\/\/doi.org\/10.1145\/2364527.2364534","DOI":"10.1145\/2364527.2364534"},{"key":"29_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-36576-1_16","volume-title":"Foundations of Software Science and Computation Structures","author":"J Dunfield","year":"2003","unstructured":"Dunfield, J., Pfenning, F.: Type assignment for intersections and unions in call-by-value languages. In: Gordon, A.D. (ed.) FoSSaCS 2003. LNCS, vol. 2620, pp. 250\u2013266. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36576-1_16"},{"issue":"5","key":"29_CR25","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1017\/S0956796803004970","volume":"14","author":"M Florido","year":"2004","unstructured":"Florido, M., Damas, L.: Linearization of the lambda-calculus and its relation with intersection type systems. J. Funct. Program. 14(5), 519\u2013546 (2004). https:\/\/doi.org\/10.1017\/S0956796803004970","journal-title":"J. Funct. Program."},{"key":"29_CR26","doi-asserted-by":"publisher","unstructured":"Frankle, J., Osera, P.M., Walker, D., Zdancewic, S.: Example-directed synthesis: a type-theoretic interpretation. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 802\u2013815. POPL 2016. Association for Computing Machinery, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2837614.2837629","DOI":"10.1145\/2837614.2837629"},{"key":"29_CR27","doi-asserted-by":"publisher","unstructured":"Freeman, T., Pfenning, F.: Refinement types for ml. In: Proceedings of the ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation, pp. 268\u2013277. PLDI 1991. Association for Computing Machinery, New York, NY, USA (1991). https:\/\/doi.org\/10.1145\/113445.113468","DOI":"10.1145\/113445.113468"},{"key":"29_CR28","doi-asserted-by":"publisher","unstructured":"Girard, J.Y.: Une extension de \u0139interpretation de g\u00f6del a \u0139analyse, et son application a \u0139elimination des coupures dans \u0139analyse et la theorie des types. In: Fenstad, J. (ed.) Proceedings of the Second Scandinavian Logic Symposium, Studies in Logic and the Foundations of Mathematics, vol. 63, pp. 63\u201392. Elsevier (1971). https:\/\/doi.org\/10.1016\/S0049-237X(08)70843-7, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0049237X08708437","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"29_CR29","volume-title":"Proofs and Types","author":"JY Girard","year":"1989","unstructured":"Girard, J.Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge University Press, Cambridge (1989)"},{"issue":"2","key":"29_CR30","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. Program. Lang. Syst. 15(2), 253\u2013289 (1993). https:\/\/doi.org\/10.1145\/169701.169692","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"29_CR31","doi-asserted-by":"crossref","unstructured":"Hindley, J.R.: Basic Simple Type Theory. Cambridge University Press (1997)","DOI":"10.1017\/CBO9780511608865"},{"key":"29_CR32","unstructured":"Jim, T.: Rank 2 type systems and recursive definitions. Technical report, Cambridge, MA, USA (1995)"},{"key":"29_CR33","doi-asserted-by":"publisher","unstructured":"Jim, T.: What are principal typings and what are they good for ? In: Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 42\u201353. POPL 1996. ACM, New York, NY, USA (1996). https:\/\/doi.org\/10.1145\/237721.237728","DOI":"10.1145\/237721.237728"},{"issue":"2","key":"29_CR34","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1145\/169701.169687","volume":"15","author":"AJ Kfoury","year":"1993","unstructured":"Kfoury, A.J., Tiuryn, J., Urzyczyn, P.: Type reconstruction in the presence of polymorphic recursion. ACM Trans. Program. Lang. Syst. 15(2), 290\u2013311 (1993)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"29_CR35","doi-asserted-by":"publisher","unstructured":"Kfoury, A.J., Wells, J.B.: Principality and decidable type inference for finite-rank intersection types. In: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 161\u2013174. POPL 1999. ACM, New York, NY, USA (1999). https:\/\/doi.org\/10.1145\/292540.292556","DOI":"10.1145\/292540.292556"},{"issue":"1","key":"29_CR36","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2003.10.032","volume":"311","author":"A Kfoury","year":"2004","unstructured":"Kfoury, A., Wells, J.: Principality and type inference for intersection types using expansion variables. Theoret. Comput. Sci. 311(1), 1\u201370 (2004). https:\/\/doi.org\/10.1016\/j.tcs.2003.10.032","journal-title":"Theoret. Comput. Sci."},{"key":"29_CR37","doi-asserted-by":"publisher","unstructured":"Leivant, D.: Polymorphic type inference. In: Proceedings of the 10th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 88\u201398. POPL 1983. Association for Computing Machinery, New York, NY, USA (1983). https:\/\/doi.org\/10.1145\/567067.567077","DOI":"10.1145\/567067.567077"},{"issue":"3","key":"29_CR38","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1017\/S095679680100394X","volume":"11","author":"J Palsberg","year":"2001","unstructured":"Palsberg, J., Pavlopoulou, C.: From polyvariant flow information to intersection and union types. J. Funct. Program. 11(3), 263\u2013317 (2001). https:\/\/doi.org\/10.1017\/S095679680100394X","journal-title":"J. Funct. Program."},{"key":"29_CR39","unstructured":"Pierce, B.C.: Types and Programming Languages. The MIT Press, 1st edn. (2002)"},{"key":"29_CR40","unstructured":"Pottinger, G.: A type assignment for the strongly normalizable lambda-terms. In: Hindley, J., Seldin, J. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 561\u2013577. Academic Press (1980)"},{"key":"29_CR41","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Towards a theory of type structure. In: Programming Symposium, Proceedings Colloque Sur La Programmation, pp. 408\u2013423. Springer-Verlag, Berlin, Heidelberg (1974). https:\/\/doi.org\/10.1007\/3-540-06859-7_148","DOI":"10.1007\/3-540-06859-7_148"},{"key":"29_CR42","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Design of the Programming Language Forsythe, pp. 173\u2013233. Birkh\u00e4user Boston, Boston, MA (1997). https:\/\/doi.org\/10.1007\/978-1-4612-4118-8_9","DOI":"10.1007\/978-1-4612-4118-8_9"},{"issue":"1","key":"29_CR43","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23\u201341 (1965). https:\/\/doi.org\/10.1145\/321250.321253","journal-title":"J. ACM"},{"key":"29_CR44","doi-asserted-by":"publisher","unstructured":"Ronchi Della Rocca, S.: Principal type scheme and unification for intersection type discipline. Theor. Comput. Sci. 59(1\u20132), 181\u2013209 (1988). https:\/\/doi.org\/10.1016\/0304-3975(88)90101-6","DOI":"10.1016\/0304-3975(88)90101-6"},{"key":"29_CR45","doi-asserted-by":"publisher","unstructured":"Urzyczyn, P.: The emptiness problem for intersection types. In: Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, pp. 300\u2013309 (1994). https:\/\/doi.org\/10.1109\/LICS.1994.316059","DOI":"10.1109\/LICS.1994.316059"},{"key":"29_CR46","volume-title":"Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting Systems","author":"SJ Van Bakel","year":"1993","unstructured":"Van Bakel, S.J.: Intersection Type Disciplines in Lambda Calculus and Applicative Term Rewriting Systems. Mathematisch Centrum, Amsterdam (1993)"},{"issue":"2","key":"29_CR47","first-page":"115","volume":"10","author":"M Wand","year":"1987","unstructured":"Wand, M.: A simple algorithm and proof for type inference. Fund. Inform. 10(2), 115\u2013121 (1987)","journal-title":"Fund. Inform."}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2022"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-17715-6_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,2]],"date-time":"2022-10-02T23:05:19Z","timestamp":1664751919000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-17715-6_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031177149","9783031177156"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-17715-6_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"3 October 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Theoretical Aspects of Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tbilisi","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Georgia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 September 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ictac2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/viam.science.tsu.ge\/clas2022\/ictac\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}