paper-conference

Gradient: Gradual Compartmentalization via Object Capabilities Tracked in Types
Modern software needs fine-grained compartmentalization, i.e., intra-process isolation. A particularly important reason for it are …
Alex Boruch⁠-⁠Gruszecki, Adrien Ghosn, Mathias Payer, Clément Pit-Claudel
PDF Video DOI
When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism
Type inference in the presence of first-class or “impredicative” second-order polymorphism à la System F has been an active research …
Lionel Parreaux, Alex Boruch⁠-⁠Gruszecki, Andong Fan, Chun Yin Chau
PDF DOI
A case for DOT: Theoretical Foundations for Objects with Pattern Matching and GADT-style Reasoning
Many programming languages in the OO tradition now support pattern matching in some form. Historical examples include Scala and Ceylon, …
Alex Boruch⁠-⁠Gruszecki, Radosław Waśko, Yichen Xu, Lionel Parreaux
PDF DOI
Effects, capabilities, and boxes: from scope-based reasoning to type-based reasoning and back
Reasoning about the use of external resources is an important aspect of many practical applications. Effect systems enable tracking …
Jonathan Brachthäuser, Philipp Schuster, Edward Lee, Alex Boruch⁠-⁠Gruszecki
PDF DOI