[SIGPLAN OOPSLA’25] Complete the Cycle: Reachability Types with Expressive Cyclic References
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 JunDisplayed time zone: Mountain Time (US & Canada) change
16:10 - 17:50 | |||
16:10 20mTalk | [SIGPLAN PLDI’25] Probabilistic Refinement Session Types PLDI Research Papers | ||
16:30 20mTalk | [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 20mTalk | 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 20mTalk | 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 20mTalk | Syntactic Implicit Parameters with Static Overloading PLDI Research Papers DOI Pre-print | ||