{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:06:48Z","timestamp":1760044008426,"version":"3.41.0"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T00:00:00Z","timestamp":1714348800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,4,29]]},"abstract":"<jats:p>Type qualifiers offer a lightweight mechanism for enriching existing type systems to enforce additional, desirable, program invariants. They do so by offering a restricted but effective form of subtyping. While the theory of type qualifiers is well understood and present in many programming languages today, polymorphism over type qualifiers remains an area less well examined. We explore how such a polymorphic system could arise by constructing a calculus, System F-sub-Q, which combines the higher-rank bounded polymorphism of System F-sub with the theory of type qualifiers. We explore how the ideas used to construct System F-sub-Q can be reused in situations where type qualifiers naturally arise---in reference immutability, function colouring, and capture checking. Finally, we re-examine other qualifier systems in the literature in light of the observations presented while developing System F-sub-Q.<\/jats:p>","DOI":"10.1145\/3649832","type":"journal-article","created":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T17:53:50Z","timestamp":1714413230000},"page":"583-612","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Qualifying System F<sub>&lt;:<\/sub>: Some Terms and Conditions May Apply"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7057-0912","authenticated-orcid":false,"given":"Edward","family":"Lee","sequence":"first","affiliation":[{"name":"University of Waterloo, Waterloo, Canada"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2257-1413","authenticated-orcid":false,"given":"Yaoyu","family":"Zhao","sequence":"additional","affiliation":[{"name":"EPFL, Lausanne, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9066-1889","authenticated-orcid":false,"given":"Ond\u0159ej","family":"Lhot\u00e1k","sequence":"additional","affiliation":[{"name":"University of Waterloo, Waterloo, Canada"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-5906-0305","authenticated-orcid":false,"given":"James","family":"You","sequence":"additional","affiliation":[{"name":"University of Waterloo, Waterloo, Canada"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-1106-2429","authenticated-orcid":false,"given":"Kavin","family":"Satheeskumar","sequence":"additional","affiliation":[{"name":"University of Waterloo, Waterloo, Canada"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9128-0391","authenticated-orcid":false,"given":"Jonathan Immanuel","family":"Brachth\u00e4user","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, T\u00fcbingen, Germany"}]}],"member":"320","published-online":{"date-parts":[[2024,4,29]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"Scott Aaronson. 2002. Polynomial Hierarchy Collapses: Thousands Feared Tractable. https:\/\/scottaaronson.com\/writings\/phcollapse.pdf"},{"volume-title":"The essence of dependent object types. A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, 249\u2013272","author":"Amin Nada","key":"e_1_2_2_2_1","unstructured":"Nada Amin, Samuel Gr\u00fctter, Martin Odersky, Tiark Rompf, and Sandro Stucki. 2016. The essence of dependent object types. A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, 249\u2013272."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328443"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485516"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500070109"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3618003"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.5381\/JOT.2006.5.5.A1"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3386323"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54415-1_73"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2824815.2824816"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/365230.365252"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985889"},{"key":"e_1_2_2_13_1","unstructured":"Stephen Dolan. 2016. Algebraic subtyping. Ph. D. Dissertation."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.18"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41654"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/301618.301665"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512531"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","unstructured":"Nikolaos Galatos. 2023. Decidability of Lattice Equations. https:\/\/doi.org\/10.1007\/s11225-023-10063-4 10.1007\/s11225-023-10063-4","DOI":"10.1007\/s11225-023-10063-4"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3359591.3359731"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450272"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39038-8_8"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384619"},{"key":"e_1_2_2_23_1","volume-title":"Java SE 8 Edition","author":"Gosling James","unstructured":"James Gosling, Bill Joy, Guy L. Steele, Gilad Bracha, and Alex Buckley. 2014. The Java Language Specification, Java SE 8 Edition (1st ed.). Addison-Wesley Professional. isbn:013390069X","edition":"1"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384680"},{"key":"e_1_2_2_25_1","doi-asserted-by":"crossref","unstructured":"Peter Jipsen. 2001. A Gentzen system and decidability for residuated lattices. Preprint https:\/\/www1.chapman.edu\/~jipsen\/reslat\/gentzenrl.pdf","DOI":"10.1007\/978-1-4757-3627-4_3"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1984.10001"},{"key":"e_1_2_2_27_1","volume-title":"Kernighan and Dennis Ritchie","author":"Brian","year":"1988","unstructured":"Brian W. Kernighan and Dennis Ritchie. 1988. The C Programming Language, Second Edition. Prentice-Hall. isbn:0-13-110370-9 https:\/\/en.wikipedia.org\/wiki\/The_C_Programming_Language"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622828"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3605156.3606454"},{"key":"e_1_2_2_30_1","volume-title":"Artifact for the OOPSLA 2024 paper \u2019Qualifying System F-sub\u2019. https:\/\/archive.softwareheritage.org\/swh:1:snp:25948423337bcc31981da471b67258ff572a5585","author":"Lee Edward","year":"2024","unstructured":"Edward Lee, Yaoyu Zhao, Ond\u0159ej Lhot\u00e1k, James You, Kavin Satheeskumar, and Jonathan Immanuel Brachth\u00e4user. 2024. Artifact for the OOPSLA 2024 paper \u2019Qualifying System F-sub\u2019. https:\/\/archive.softwareheritage.org\/swh:1:snp:25948423337bcc31981da471b67258ff572a5585"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3580431"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.153.8"},{"key":"e_1_2_2_33_1","unstructured":"Daan Leijen and Ross Tate. 2010. Convenient Explicit Effects using Type Inference with Subeffects. https:\/\/www.microsoft.com\/en-us\/research\/publication\/convenient-explicit-effects-using-type-inference-with-subeffects\/"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/567067.567077"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73564"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607846"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485487"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1667048.1667049"},{"key":"e_1_2_2_39_1","unstructured":"Jens Maurer. 2015. P0012R1: Make exception specifications be part of the type system version 5. https:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2015\/p0012r1.html"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s000120200012"},{"key":"e_1_2_2_41_1","unstructured":"Bob Nystrom. 2015. What Color is Your Function? https:\/\/journal.stuffwithstuff.com\/2015\/02\/01\/what-color-is-your-function\/"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3486610.3486893"},{"key":"e_1_2_2_43_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_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984009"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390656"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628160"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36946-9_9"},{"key":"e_1_2_2_48_1","volume-title":"Lightweight Polymorphic Effects. In ECOOP 2012 \u2013 Object-Oriented Programming, James Noble (Ed.). Springer Berlin Heidelberg","author":"Rytz Lukas","year":"2012","unstructured":"Lukas Rytz, Martin Odersky, and Philipp Haller. 2012. Lightweight Polymorphic Effects. In ECOOP 2012 \u2013 Object-Oriented Programming, James Noble (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 258\u2013282. isbn:978-3-642-31057-7"},{"key":"e_1_2_2_49_1","unstructured":"Thoralf Skolem. 1920. Logisch-Kombinatorische Untersuchungen \u00dcber Die Erf\u00fcllbarkeit Oder Bewiesbarkeit Mathematischer S\u00e4tze Nebst Einem Theorem \u00dcber Dichte Mengen. In Selected Works in Logic Thoralf Skolem (Ed.). Universitetsforlaget."},{"key":"e_1_2_2_50_1","unstructured":"Max Slater. 2023. Oxidizing OCaml: Rust-Style Ownership. https:\/\/blog.janestreet.com\/oxidizing-ocaml-ownership\/"},{"volume-title":"The C++ programming language - special edition (3. ed.)","author":"Stroustrup Bjarne","key":"e_1_2_2_51_1","unstructured":"Bjarne Stroustrup. 2007. The C++ programming language - special edition (3. ed.). Addison-Wesley. isbn:978-0-201-70073-2"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094828"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632856"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.2307\/1969001"},{"key":"e_1_2_2_55_1","unstructured":"Yoshua Wuyts Oli Scherer and Niko Matsakis. 2022. Announcing the keyword generics initiative: Inside rust blog. https:\/\/blog.rust-lang.org\/inside-rust\/2022\/07\/27\/keyword-generics.html"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2022.15"},{"key":"e_1_2_2_57_1","unstructured":"Yaoyu Zhao. 2023. Adding Reference Immutability to Scala. Master\u2019s thesis. http:\/\/hdl.handle.net\/10012\/19601"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1287624.1287637"},{"key":"e_1_2_2_59_1","volume-title":"OOPSLA","author":"Zibin Yoav","year":"2010","unstructured":"Yoav Zibin, Alex Potanin, Paley Li, Mahmood Ali, and Michael D. Ernst. 2010. Ownership and immutability in generic Java. In OOPSLA 2010, Object-Oriented Programming Systems, Languages, and Applications. Reno, NV, USA. 598\u2013617."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649832","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649832","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:06Z","timestamp":1750287246000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649832"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,29]]},"references-count":59,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2024,4,29]]}},"alternative-id":["10.1145\/3649832"],"URL":"https:\/\/doi.org\/10.1145\/3649832","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2024,4,29]]},"assertion":[{"value":"2024-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}