Скачать или смотреть [OOPSLA'25] Qualified Types with Boolean Algebras

Qualified Types with Boolean Algebras (Video, OOPSLA2 2025)
Edward Lee, Jonathan Lindegaard Starup, Ondřej Lhoták, and Magnus Madsen
(University of Waterloo, Canada; Aarhus University, Denmark; University of Waterloo, Canada; Aarhus University, Denmark)

Abstract: 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.


In this paper, we present a calculus System F⧼:B that extends System F⧼: with type qualifiers over Boolean algebras and has support for negation, qualifier polymorphism, and subqualification. We illustrate how System F⧼:B can be used as a design recipe for a type and effect system, System F⧼:BE, with effect polymorphism, subeffecting, and polymorphic effect exclusion. We use System F

Article: https://doi.org/10.1145/3763096

Supplementary archive: https://doi.org/10.5281/zenodo.16915676 (Badges: Artifacts Available, Artifacts Evaluated — Reusable, Results Reproduced)

ORCID: https://orcid.org/0000-0001-7057-0912, https://orcid.org/0000-0002-0931-7878, https://orcid.org/0000-0001-9066-1889, https://orcid.org/0000-0002-7510-8724

Video Tags: Boolean Algebras, Flix, System F⧼:, Type Qualifiers, Type Systems, oopslab25main-p385-p, doi:10.1145/3763096, doi:10.5281/zenodo.16915676, orcid:0000-0001-7057-0912, orcid:0000-0002-0931-7878, orcid:0000-0001-9066-1889, orcid:0000-0002-7510-8724, Artifacts Available, Artifacts Evaluated — Reusable, Results Reproduced

Presentation at the OOPSLA2 2025 conference, October 13–15, https://2025.splashcon.org/track/OOPSLA
Sponsored by ACM SIGPLAN,