Type Systems

Modular Type Safety for Traits with Extensible Variants and Deep Pattern Matching
Traits provide a powerful mechanism for code reuse by allowing the definition of shared behaviors that can be composed into classes. …
Cite
First-Class Constrained Types
We study a first-class treatment of constrained types, which were previously confined mostly to ML-style polymorphism. We define System …
Cite View conference website
The Simple Essence of Boolean-Algebraic Subtyping
Boolean-algebraic subtyping (BAS) is a powerful subtyping approach introduced in 2022 as the “secret sauce” enabling backtracking-free …
PDF Cite Code Video DOI View on conference website Web demonstration
When Subtyping Constraints Liberate
Type inference in the presence of first-class or “impredicative” second-order polymorphism à la System F has been an active research …
PDF Cite DOI Github Project Tech. Report PDF View on conference website
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, …
PDF Cite Video DOI Github Project Tech. Report PDF View on conference website
Type-Safe Metaprogramming and Compilation Techniques For Designing Efficient Systems in High-Level Languages
Software engineering practices have been steadily moving towards higher-level programming languages and away from lower-level ones. …
Cite DOI
The Simple Essence of Algebraic Subtyping
MLsub extends traditional Hindley-Milner type inference with subtyping while preserving compact principal types, an exciting new …
PDF Cite Video DOI Github Project View on conference website
Unifying Analytic and Statically-Typed Quasiquotes
Metaprograms are programs that manipulate (generate, analyze and evaluate) other programs. These tasks are greatly facilitated by …
PDF Cite Video DOI Github Project