Reachability Types

Reachability types are a new take on modeling lifetimes and sharing in high-level functional languages, showing how to integrate Rust-style reasoning capabilities with higher-order functions, polymorphic types, and similar high-level abstractions.

Mechanization Overview

• base -- Coq mechanization of the $λ^*$-calculus [1] and its variations, gradually increasing in complexity.

• effects -- Coq mechanization of the $λ_\varepsilon^*$-calculus [1] and its variations, gradually increasing in complexity.

• polymorphism -- Coq mechanization of the $λ^\diamond$-calculus [2] and its variations, featuring a refined reachability model that scales to parametric type polymorphism.

• log-rel-experiment -- Experimenting semantic models of $λ^\diamond$, $λ_\varepsilon^\diamond$, and its variants [4,5].

• log-rel -- Unary/Binary logical relations for proving semantic type soundness and termination of $λ^\diamond$, $λ_\varepsilon^\diamond$, as well as proofs of equational rules [4].

• log-rel-step-indexed -- Step-indexed logical relations for $λ^\diamond$, $λ_\varepsilon^\diamond$ and its variants [4].

• checking -- Bidirectional type system $\lambda^\diamond_R$ with decidable type checking/inference, including refined subtyping for self-references [5]

• cycles -- Bounded type-and-reachability polymorphism with cyclic references and natural numbers [6].

• arena -- Region-based resource management, cyclic store structures via coarse-grained reachability tracking, and scoped deallocation reasoning [7].

Prototype Implementations

• Interactive prototype for [1], also demonstrating the use of reachability types for graph-based IRs for impure functional languages [3].

• A standalone prototype language Diamond implements polymorphic reachability types [2].

Contributors

• Oliver Bračevac (Initial mechanization lead 2021-2022)
• Guannan Wei (Polymorphism lead 2023-2024)
• Yuyan Bao (Logical relations lead 2023-2025)
• Songlin Jia (Type checking lead 2024-2025)
• Siyuan He (Arena lead 2024-2025)
• David Deng
• Yueyang Tang
• Tiark Rompf

References

[1] Reachability Types: Tracking Aliasing and Separation in Higher-order Functional Programs (OOPSLA 2021)
Yuyan Bao, Guannan Wei, Oliver Bračevac, Luke Jiang, Qiyang He, Tiark Rompf (pdf).

[2] Polymorphic Reachability Types: Tracking Aliasing and Separation in Higher-order Generic Programs (POPL 2024)
Guannan Wei, Oliver Bračevac, Siyuan He, Yuyan Bao, Tiark Rompf (pdf).

[3] Graph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Affordable with Precise Effect Dependencies (OOPSLA 2023)
Oliver Bračevac, Guannan Wei, Luke Jiang, Supun Abeysinghe, Songlin Jia, Siyuan He, Yuyan Bao, Tiark Rompf (pdf).

[4] Modeling Reachability Types with Logical Relations: Semantic Type Soundness, Termination, and Equational Theory (OOPSLA 2025)
Yuyan Bao, Songlin Jia, Guannan Wei, Oliver Bračevac, Tiark Rompf (pdf).

[5] Complete the Cycle: Reachability Types with Expressive Cyclic References (OOPSLA 2025)
Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf (pdf).

[6] Escape with Your Self: Expressive Reachability Types with Sound and Decidable Bidirectional Type Checking (Tech Report 2025)
Songlin Jia, Guannan Wei, Siyuan He, Yuyan Bao, Tiark Rompf (pdf).

[7] When Lifetimes Liberate: A Type System for Arenas with Higher-Order Reachability Tracking (Tech Report 2025)
Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf (pdf)

[8] Free to Move: Reachability Types with Flow-Sensitive Effects for Safe Deallocation and Ownership Transfer (Tech Report 2025)
Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf (pdf)

[9] Typestate via Revocable Capabilities (Tech Report 2025)
Songlin Jia, Craig Liu, Siyuan He, Haotian Deng, Yuyan Bao, Tiark Rompf (pdf)

[10] Type, Ability, and Effect Systems: Perspectives on Purity, Semantics, and Expressiveness (Tech Report 2025)
Yuyan Bao, Tiark Rompf (pdf)