October 23, 2025
Reachability types enable static, type-level reasoning about resource usage. Unlike designs that require unique or linear access paths, reachability types apply to higher-order, impure languages with pervasive sharing. They have been demonstrated to enforce safe parallelism, guide compiler optimizations, and ensure scoped resource lifetimes.
Nevertheless, typing algorithms for reachability types are complicated by the notion of self-references. Unlike ordinary variables, which appear in qualifiers to denote external resources, self-references denote internal reachability (akin to this in OO languages) at the type level. They are essential for preserving well-scoped qualifiers (avoidance) and for encoding data structures. However, their subqualifying behavior is inverted relative to ordinary variables, their avoidance has not previously been expressible solely via subtyping, and they complicate automatic inference of term-level qualifiers.
In this work, we present the first algorithmic scheme for reachability types, with mechanized soundness proof via logical relations in Lean. The scheme employs a decidable subqualifying relation and a unified type-and-qualifier subtyping discipline. Built on this foundation, avoidance is expressed purely via subtyping and applied automatically when variables leave scope. Furthermore, we introduce a bidirectional inference strategy that permits gradual instantiation of term-level qualifiers. Looking forward, we show how the design extends to implicit type-and-qualifier instantiation and to encoding algebraic data types.
About Songlin Jia
Songlin Jia is a fifth-year PhD student in Computer Science, working with Professor Tiark Rompf. He has been working on a wide range of topics in his early years, including program analysis, symbolic execution, scientific computing, and compilers. Recently, he is interested in type systems that track resources and effects.