{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:10:12Z","timestamp":1784200212691,"version":"3.55.0"},"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>\n                    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\n                    <jats:italic toggle=\"yes\">exclusion<\/jats:italic>\n                    . We argue that Boolean algebras, which permit exclusion, are a practical and useful choice of domain for qualifiers.\n                  <\/jats:p>\n                  <jats:p>\n                    In this paper, we present a calculus System F\n                    <jats:sub>&lt;:B<\/jats:sub>\n                    that extends System F\n                    <jats:sub>&lt;:<\/jats:sub>\n                    with type qualifiers over Boolean algebras and has support for negation, qualifier polymorphism, and subqualification. We illustrate how System F\n                    <jats:sub>&lt;:B<\/jats:sub>\n                    can be used as a design recipe for a type and effect system, System F\n                    <jats:sub>&lt;:BE<\/jats:sub>\n                    , with effect polymorphism, subeffecting, and polymorphic effect exclusion. We use System F\n                    <jats:sub>&lt;:BE<\/jats:sub>\n                    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.\n                  <\/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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7510-8724","authenticated-orcid":false,"given":"Magnus","family":"Madsen","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","unstructured":"Brian Aydemir Arthur Chargu\u00e9raud Benjamin C. Pierce Randy Pollack and Stephanie Weirich. 2008. Engineering formal metatheory. In Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. doi:10.1145\/1328438.1328443 14","DOI":"10.1145\/1328438.1328443"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/s0020-0190(98)00106-9"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2014.02.001"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/s1571-0661(04)80803-x"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","unstructured":"Robert L. Bocchino Vikram S. Adve Danny Dig Sarita V. Adve Stephen Heumann Rakesh Komuravelli Jeffrey Overbey Patrick Simmons Hyojin Sung and Mohsen Vakilian. 2009. A type and effect system for deterministic parallel Java. In Proceedings of the 24th ACM SIGPLAN conference on Object oriented programming systems languages and applications. doi:10.1145\/1640089.1640097 25","DOI":"10.1145\/1640089.1640097"},{"key":"e_1_3_1_7_2","unstructured":"George Boole. 1847. The mathematical analysis of logic. 18 24"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3618003"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/s0747-7171(89)80054-9"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/3527320"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428194"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/s0747-7171(87)80065-2"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","unstructured":"Werner Dietl Stephanie Dietzel Michael D. Ernst Kivan\u00e7 Mu\u015flu and Todd W. Schiller. 2011. Building and using pluggable type-checkers. In Proceedings of the 33rd International Conference on Software Engineering. doi:10.1145\/1985793.198588923","DOI":"10.1145\/1985793.198588923"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","unstructured":"Stephen Dolan and Alan Mycroft. 2017. Polymorphism subtyping and type inference in MLsub. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. doi:10.1145\/3009837.3009882 24","DOI":"10.1145\/3009837.3009882"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","unstructured":"M. Felleisen and D. P. Friedman. 1987. A calculus for assignments in higher-order languages. In Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages - POPL \u201987. doi:10.1145\/41625.41654 11 13","DOI":"10.1145\/41625.41654"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","unstructured":"Jeffrey S. Foster Manuel F\u00e4hndrich and Alexander Aiken. 1999. A theory of type qualifiers. In Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation. doi:10.1145\/301618.301665 1 7 8 10 23","DOI":"10.1145\/301618.301665"},{"key":"e_1_3_1_17_2","doi-asserted-by":"crossref","unstructured":"Tim Freeman and Frank Pfenning. 1991. Refinement types for ML. In Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation. 5","DOI":"10.1145\/113445.113468"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","unstructured":"Isaac Oscar Gariano James Noble and Marco Servetto. 2019. Call \u03b5 : an effect system for method calls. In Proceedings of the 2019 ACM SIGPLAN International Symposium on New Ideas New Paradigms and Reflections on Programming and Software. doi:10.1145\/3359591.3359731 23","DOI":"10.1145\/3359591.3359731"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","unstructured":"Colin S. Gordon. 2017. A Generic Approach to Flow-Sensitive Polymorphic Effects. doi:10.4230\/LIPICS.ECOOP.2017.13 25","DOI":"10.4230\/LIPICS.ECOOP.2017.13"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3450272"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48743-3_10"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","unstructured":"Daniel Hillerstr\u00f6m and Sam Lindley. 2016. Liberating effects with rows and handlers. In Proceedings of the 1st International Workshop on Type-Driven Development. doi:10.1145\/2976022.2976033 19","DOI":"10.1145\/2976022.2976033"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","unstructured":"Wei Huang Ana Milanova Werner Dietl and Michael D. Ernst. 2012. Reim & ReImInfer: checking and inference of reference immutability and method purity. In Proceedings of the ACM international conference on Object oriented programming systems languages and applications. doi:10.1145\/2384616.2384680 23","DOI":"10.1145\/2384616.2384680"},{"key":"e_1_3_1_24_2","unstructured":"Edward Lee Ond\u0159ej Lhot\u00e1k Jonathan Lindegaard Starup and Magnus Madsen. 2025. Qualified Types with Boolean Algebras (Artifact). 2 25"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","unstructured":"Edward Lee Ond\u0159ej Lhot\u00e1k Jonathan Lindegaard Starup and Magnus Madsen. 2025. Qualified Types with Boolean Algebras (Artifact). doi:10.5281\/zenodo.16915676 2 25","DOI":"10.5281\/zenodo.16915676"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3649832"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.153.8"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","unstructured":"Sam Lindley and James Cheney. 2012. Row-based effect types for database integration. In Proceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation. doi:10.1145\/2103786.2103798 19","DOI":"10.1145\/2103786.2103798"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","unstructured":"Sam Lindley Conor McBride and Craig McLaughlin. 2017. Do be do be do. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. doi:10.1145\/3009837.3009897 19","DOI":"10.1145\/3009837.3009897"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656393"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3607846"},{"key":"e_1_3_1_32_2","unstructured":"Leopold L\u00f6wenheim. 1908. \u00dcber das Aufl\u00f6sungsproblem im logischen Klassenkalkul. 18 24"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3689770"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428193"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","unstructured":"Magnus Madsen Jonathan Lindegaard Starup and Matthew Lutze. 2023. Restrictable Variants: A Simple and Practical Alternative to Extensible Variants. doi:10.4230\/LIPICS.ECOOP.2023.17 2 3 5 6","DOI":"10.4230\/LIPICS.ECOOP.2023.17"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428222"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3485487"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622816"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","unstructured":"Daniel Marino and Todd Millstein. 2009. A generic type-and-effect system. In Proceedings of the 4th international workshop on Types in language design and implementation. doi:10.1145\/1481861.1481868 1","DOI":"10.1145\/1481861.1481868"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/1667048.1667049"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622831"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","unstructured":"Matthew M. Papi Mahmood Ali Telmo Luis Correa Jeff H. Perkins and Michael D. Ernst. 2008. Practical pluggable types for Java. In Proceedings of the 2008 international symposium on Software testing and analysis. doi:10.1145\/1390630.1390656 1","DOI":"10.1145\/1390630.1390656"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3409006"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3563304"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","unstructured":"Xin Qi and Andrew C. Myers. 2009. Masked types for sound object initialization. In Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. doi:10.1145\/1480881.1480890 24","DOI":"10.1145\/1480881.1480890"},{"key":"e_1_3_1_46_2","unstructured":"Sergiu Rudeanu. 1974. Boolean functions and equations. 24"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31057-7_13"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1017\/s0956796800000393"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/3689750"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","unstructured":"Matthew S. Tschantz and Michael D. Ernst. 2005. Javari: adding reference immutability to Java. In Proceedings of the 20th annual ACM SIGPLAN conference on Object-oriented programming systems languages and applications. doi:10.1145\/1094811.1094828 23","DOI":"10.1145\/1094811.1094828"},{"key":"e_1_3_1_51_2","volume-title":"Complete Type Inference for Simple Objects. In 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. 24"},{"key":"e_1_3_1_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632856"},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/3408981"},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","unstructured":"Yoav Zibin Alex Potanin Mahmood Ali Shay Artzi Adam Kiezun and Michael D. Ernst. 2007. Object and reference immutability using Java generics. In Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering. doi:10.1145\/1287624.1287637 23","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":[[2026,7,16]],"date-time":"2026-07-16T10:12:41Z","timestamp":1784196761000},"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"}}]}}