{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T18:11:35Z","timestamp":1760033495993,"version":"build-2065373602"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>We propose type qualifiers based on Boolean algebras. Traditional type systems with type qualifiers have been based on lattices, but lattices lack the ability to express exclusion. We argue that Boolean algebras, which permit exclusion, are a practical and useful choice of domain for qualifiers.<\/jats:p>\n          <jats:p>In this paper, we present a calculus System F&lt;:B that extends System F&lt;: with type qualifiers over Boolean algebras and has support for negation, qualifier polymorphism, and subqualification. We illustrate how System F&lt;:B can be used as a design recipe for a type and effect system, System F&lt;:BE, with effect polymorphism, subeffecting, and polymorphic effect exclusion. We use System F&lt;:BE to establish formal foundations of the type and effect system of the Flix programming language. We also pinpoint and implement a practical form of subeffecting: abstraction-site subeffecting. Experimental results show that abstraction-site subeffecting allows us to eliminate all effect upcasts present in the current Flix Standard Library.<\/jats:p>","DOI":"10.1145\/3763096","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:51:31Z","timestamp":1759999891000},"page":"1289-1315","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Qualified Types with Boolean Algebras"],"prefix":"10.1145","volume":"9","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"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0931-7878","authenticated-orcid":false,"given":"Jonathan Lindegaard","family":"Starup","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"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"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7510-8724","authenticated-orcid":false,"given":"Magnus","family":"Madsen","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328443"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/s0020-0190(98)00106-9"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","unstructured":"G. M. Bierman and M. J. Parkinson. 2003. Effects and effect inference for a core Java calculus. Electronic Notes in Theoretical Computer Science 82 8 (2003) https:\/\/doi.org\/10.1016\/s1571-0661(04)80803-x 10.1016\/s1571-0661(04)80803-x","DOI":"10.1016\/s1571-0661(04)80803-x"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1640089.1640097"},{"key":"e_1_2_1_6_1","unstructured":"George Boole. 1847. The mathematical analysis of logic."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3618003"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/s0747-7171(89)80054-9"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527320"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428194"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/s0747-7171(87)80065-2"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985889"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009882"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41654"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/301618.301665"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3359591.3359731"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","unstructured":"Colin S. Gordon. 2017. A Generic Approach to Flow-Sensitive Polymorphic Effects. https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2017.13 10.4230\/LIPICS.ECOOP.2017.13","DOI":"10.4230\/LIPICS.ECOOP.2017.13"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450272"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48743-3_10"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976022.2976033"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384680"},{"key":"e_1_2_1_23_1","volume-title":"Jonathan Lindegaard Starup, and Magnus Madsen","author":"Lee Edward","year":"2025","unstructured":"Edward Lee, Ond\u0159ej Lhot\u00e1k, Jonathan Lindegaard Starup, and Magnus Madsen. 2025. Qualified Types with Boolean Algebras (Artifact)."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.16915676"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649832"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.153.8"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103786.2103798"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009897"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656393"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607846"},{"key":"e_1_2_1_31_1","unstructured":"Leopold L\u00f6wenheim. 1908. \u00dcber das Aufl\u00f6sungsproblem im logischen Klassenkalkul."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689770"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428193"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2023.17"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428222"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485487"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622816"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481868"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1667048.1667049"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622831"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390656"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409006"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563304"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480890"},{"key":"e_1_2_1_45_1","unstructured":"Sergiu Rudeanu. 1974. Boolean functions and equations."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31057-7_13"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1017\/s0956796800000393"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689750"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094828"},{"key":"e_1_2_1_50_1","volume-title":"Proceedings of the Symposium on Logic in Computer Science (LICS\u201987)","author":"Wand Mitchell","year":"1987","unstructured":"Mitchell Wand. 1987. Complete Type Inference for Simple Objects. In Proceedings of the Symposium on Logic in Computer Science (LICS\u201987), Ithaca, New York, USA, June 22-25, 1987."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632856"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408981"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1287624.1287637"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763096","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:40:09Z","timestamp":1760031609000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763096"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":53,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763096"],"URL":"https:\/\/doi.org\/10.1145\/3763096","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-25","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}