Wed 17 Jun 2026 16:30 - 16:50 at Flatirons 4 - Type Systems Chair(s): Eleftherios Ioannidis

Local reasoning about programs that combine aliasing and mutable state is a longstanding challenge. Existing approaches – ownership systems, linear and affine types, uniqueness types, and lexical effect tracking – impose global restrictions such as uniqueness or linearity, or rely on shallow syntactic analyses. These designs fall short with higher-order functions and shared mutable state. Reachability Types (RT) track aliasing and separation in higher-order programs, ensuring runtime safety and non-interference. However, RT systems face three key limitations: (1) they prohibit cyclic references, ruling out non-terminating computations and fixed-point combinators; (2) they require deep tracking, where a qualifier must include all transitively reachable locations, reducing precision and hindering optimizations like fine-grained parallelism; and (3) referent qualifier invariance prevents referents from escaping their allocation contexts, making reference factories inexpressible.\nIn this work, we address these limitations by extending RT with three mechanisms that enhance expressiveness. First, we introduce cyclic references, enabling recursive patterns to be encoded directly through the store. Second, we adopt shallow qualifier tracking, decoupling references from their transitively reachable values. Finally, we introduce an escaping rule with reference subtyping, allowing referent qualifiers to outlive their allocation context. These extensions are formalized in the F<:∘-calculus with a mechanized proof of type soundness, and case studies illustrate expressiveness through fixpoint combinators, non-interfering parallelism, and escaping read-only references.

Wed 17 Jun

Displayed time zone: Mountain Time (US & Canada) change

16:10 - 17:50
Type SystemsPLDI Research Papers at Flatirons 4
Chair(s): Eleftherios Ioannidis Microsoft Research
16:10
20m
Talk
[SIGPLAN PLDI’25] Probabilistic Refinement Session Types
PLDI Research Papers
Qiancheng Fu Boston University, Ankush Das Boston University, Marco Gaboardi Boston University
16:30
20m
Talk
[SIGPLAN OOPSLA’25] Complete the Cycle: Reachability Types with Expressive Cyclic References
PLDI Research Papers
Haotian Deng Purdue University, Siyuan He Purdue University, Songlin Jia Purdue University, Yuyan Bao Augusta University, Tiark Rompf Purdue University
16:50
20m
Talk
Backwards-Compatible Row-Based Exceptions in ML
PLDI Research Papers
Simcha van Collem Radboud University Nijmegen, Paulo Emílio de Vilhena University of Surrey, Robbert Krebbers Radboud University Nijmegen
DOI
17:10
20m
Talk
Typestate via Revocable Capabilities
PLDI Research Papers
Songlin Jia Purdue University, Craig Liu Purdue University, Siyuan He Purdue University, Haotian Deng Purdue University, Yuyan Bao Augusta University, Tiark Rompf Purdue University
DOI
17:30
20m
Talk
Syntactic Implicit Parameters with Static Overloading
PLDI Research Papers
Daan Leijen Microsoft Research, Tim Whiting Brigham Young University
DOI Pre-print