{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T13:55:22Z","timestamp":1787061322573,"version":"build-2736575974"},"reference-count":67,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Hong Kong Research Grant Council","award":["26208821"],"award-info":[{"award-number":["26208821"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>\n                    Type inference in the presence of\n                    <jats:italic toggle=\"yes\">first-class<\/jats:italic>\n                    or \u201c\n                    <jats:italic toggle=\"yes\">impredicative<\/jats:italic>\n                    \u201d\n                    <jats:italic toggle=\"yes\">second-order polymorphism<\/jats:italic>\n                    \u00e0 la System\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mi mathvariant=\"normal\">F<\/mml:mi>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    has been an active research area for several decades, with original works dating back to the end of the 80s. Yet, until now many basic problems remain open, such as how to type check expressions like\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mo stretchy=\"true\">(<\/mml:mo>\n                        <mml:mi mathvariant=\"italic\">\u03bb<\/mml:mi>\n                        <mml:mi mathvariant=\"italic\">x<\/mml:mi>\n                        <mml:mo>.<\/mml:mo>\n                        <mml:mo stretchy=\"true\">(<\/mml:mo>\n                        <mml:mi>x<\/mml:mi>\n                        <mml:mtext>\u2009<\/mml:mtext>\n                        <mml:mtext>\u2009<\/mml:mtext>\n                        <mml:mn>123<\/mml:mn>\n                        <mml:mo>,<\/mml:mo>\n                        <mml:mtext>\u2009<\/mml:mtext>\n                        <mml:mi>x<\/mml:mi>\n                        <mml:mtext>\u2009<\/mml:mtext>\n                        <mml:mtext>\u2009<\/mml:mtext>\n                        <mml:mtext>True<\/mml:mtext>\n                        <mml:mo stretchy=\"true\">)<\/mml:mo>\n                        <mml:mo stretchy=\"true\">)<\/mml:mo>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    id reliably. We show that a type inference approach based on\n                    <jats:italic toggle=\"yes\">multi-bounded polymorphism<\/jats:italic>\n                    , a form of implicit polymorphic subtyping with multiple lower and upper bounds, can help us resolve most of these problems in a uniquely simple and regular way. We define\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:msub>\n                          <mml:mi mathvariant=\"normal\">F<\/mml:mi>\n                          <mml:mfenced close=\"}\" open=\"{\">\n                            <mml:mo>\u2264<\/mml:mo>\n                          <\/mml:mfenced>\n                        <\/mml:msub>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    , a declarative type system derived from the existing theory of implicit coercions by Cretin and R\u00e9my (LICS 2014), and we introduce SuperF, a novel algorithm to infer polymorphic multi-bounded\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:msub>\n                          <mml:mi mathvariant=\"normal\">F<\/mml:mi>\n                          <mml:mfenced close=\"}\" open=\"{\">\n                            <mml:mo>\u2264<\/mml:mo>\n                          <\/mml:mfenced>\n                        <\/mml:msub>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    types while checking user type annotations written in the syntax of System F. We use a recursion-avoiding heuristic to guarantee termination of type inference at the cost of rejecting some valid programs, which thankfully rarely triggers in practice. We show that SuperF is vastly more powerful than all first-class-polymorphic type inference systems proposed so far, significantly advancing the state of the art in type inference for general-purpose programming languages.\n                  <\/jats:p>","DOI":"10.1145\/3632890","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T15:48:51Z","timestamp":1704469731000},"page":"1418-1450","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8805-0728","authenticated-orcid":false,"given":"Lionel","family":"Parreaux","sequence":"first","affiliation":[{"name":"HKUST, Hong Kong, Hong Kong"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5769-6684","authenticated-orcid":false,"given":"Aleksander","family":"Boruch-Gruszecki","sequence":"additional","affiliation":[{"name":"EPFL, Lausanne, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2124-9625","authenticated-orcid":false,"given":"Andong","family":"Fan","sequence":"additional","affiliation":[{"name":"HKUST, Hong Kong, Hong Kong"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0323-6644","authenticated-orcid":false,"given":"Chun Yin","family":"Chau","sequence":"additional","affiliation":[{"name":"HKUST, Hong Kong, Hong Kong"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/165180.165188"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622812"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","unstructured":"Hans-J. Boehm. 1985. Partial polymorphic type inference is undecidable. In 26th Annual Symposium on Foundations of Computer Science (sfcs 1985). 339\u2013345. https:\/\/doi.org\/10.1109\/SFCS.1985.44 10.1109\/SFCS.1985.44 \u21aa page 28","DOI":"10.1109\/SFCS.1985.44"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563342"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3471874.3472985"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951928"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055784"},{"key":"e_1_3_1_9_1","unstructured":"Julien Cretin. 2014. Erasable coercions: a unified approach to type systems. Theses. Universit\u00e9 Paris-Diderot - Paris VII. https:\/\/tel.archives-ouvertes.fr\/tel-00940511 \u21aa pages 3 and 15"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103699"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603128"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622871"},{"key":"e_1_3_1_13_1","unstructured":"Stephen Dolan. 2017. Algebraic subtyping. Ph. D. Dissertation. \u21aa pages 12 and 28"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009882"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450952"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544174.2500582"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290322"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964025"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386003"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547642"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-62503-8_12"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","unstructured":"A. Frisch G. Castagna and V. Benzaken. 2002. Semantic subtyping. In Proceedings 17th Annual IEEE Symposium on Logic in Computer Science. 137\u2013146. https:\/\/doi.org\/10.1109\/LICS.2002.1029823 10.1109\/LICS.2002.1029823 \u21aa page 7","DOI":"10.1109\/LICS.2002.1029823"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014546"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90011-0"},{"key":"e_1_3_1_25_1","first-page":"323","volume-title":"ICALP Satellite Workshops","author":"Jim Trevor","year":"2000","unstructured":"Trevor Jim. 2000. A Polar Type System. In ICALP Satellite Workshops. Citeseer, 323\u2013338. \u21aa pages 8 and 29"},{"key":"e_1_3_1_26_1","unstructured":"Oleg Kiselyov. 2013. Efficient generalization with levels (Okmij Blog). http:\/\/okmij.org\/ftp\/ML\/generalization.html#levels. Accessed: 2020-06-30. \u21aa page 9"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186031"},{"key":"e_1_3_1_28_1","doi-asserted-by":"crossref","unstructured":"Didier Le Botlan and Didier R\u00e9my. 2003. MLF: Raising ML to the power of System F. In Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming. 27\u201338. \u21aa pages 25 and 29","DOI":"10.1145\/944705.944709"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2008.12.006"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411245"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480891"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/91556.91675"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90009-0"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237729"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1096-9942(199901\/03)5:1<35::AID-TAPO4>3.0.CO;2-4"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/73141.74836"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268963"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409006"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","unstructured":"Lionel Parreaux Aleksander Boruch-Gruszecki Andong Fan and Chun Yin Chau. 2023. When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism (Artifact). https:\/\/doi.org\/10.5281\/zenodo.8424750 10.5281\/zenodo.8424750 \u21aa page 30","DOI":"10.5281\/zenodo.8424750"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3337932.3338813"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563304"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006034"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/62678.62697"},{"key":"e_1_3_1_44_1","volume-title":"Programming with intersection types and bounded polymorphism","author":"Pierce Benjamin C","year":"1991","unstructured":"Benjamin C Pierce. 1991. Programming with intersection types and bounded polymorphism. Ph. D. Dissertation. Citeseer. \u21aa page 29"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012959600223X"},{"key":"e_1_3_1_46_1","volume-title":"Research Report RR-3483","author":"Pottier Fran\u00e7ois","year":"1998","unstructured":"Fran\u00e7ois Pottier. 1998. Type Inference in the Presence of Subtyping: from Theory to Practice. Research Report RR-3483. INRIA. https:\/\/hal.inria.fr\/inria-00073205 \u21aa page 8"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360208"},{"key":"e_1_3_1_48_1","article-title":"Alg\u00e8bres Touffues. Application au Typage Polymorphe des Objets Enregistrements dans les Langages Fonctionnels","volume":"7","author":"R\u00e9my Didier","year":"1990","unstructured":"Didier R\u00e9my. 1990. Alg\u00e8bres Touffues. Application au Typage Polymorphe des Objets Enregistrements dans les Langages Fonctionnels. Th\u00e8se de doctorat. Universit\u00e9 de Paris 7. \u21aa page 9","journal-title":"Th\u00e8se de doctorat. Universit\u00e9 de Paris"},{"key":"e_1_3_1_49_1","volume-title":"Research Report RR-1766","author":"R\u00e9my Didier","year":"1992","unstructured":"Didier R\u00e9my. 1992. Extension of ML type system with a sorted equation theory on types. Research Report RR-1766. INRIA. https:\/\/hal.inria.fr\/inria-00077006 Projet FORMEL. \u21aa page 9"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.5555\/645868.668492"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1090189.1086383"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190315.1190321"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596627.1596630"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2012.02.026"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_28"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408971"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192389"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46425-5_25"},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561306"},{"key":"e_1_3_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159838"},{"key":"e_1_3_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411246"},{"key":"e_1_3_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45337-7_6"},{"key":"e_1_3_1_63_1","unstructured":"Joseph B. Wells. 1996. Type inference for System F with and without the eta rule. Ph. D. Dissertation. http:\/\/ezproxy.ust.hk\/login?url=https:\/\/www.proquest.com\/dissertations-theses\/type-inference-system-f-withwithout-eta-rule\/docview\/304323713\/se-2 Copyright - Database copyright ProQuest LLC; ProQuest does not claim copyright in the individual underlying works; Last updated - 2023-02-24. \u21aa page 28"},{"key":"e_1_3_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604150"},{"key":"e_1_3_1_65_1","unstructured":"Ningning Xie. 2021. Higher-rank polymorphism : type inference and extensions. http:\/\/hdl.handle.net\/10722\/307011 \u21aa page 27"},{"key":"e_1_3_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_10"},{"key":"e_1_3_1_67_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2021.102655"},{"key":"e_1_3_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341716"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632890","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632890","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T16:05:06Z","timestamp":1751645106000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632890"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":67,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632890"],"URL":"https:\/\/doi.org\/10.1145\/3632890","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}