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-unary -- Unary logical relations for proving semantic type soundness and termination of $λ^\diamond$, $λ_\varepsilon^\diamond$, and its variants [4,5].

• log-rel-binary -- Binary logical relations for establishing equational reasoning about $λ^\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]

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-2024)
• Songlin Jia
• Siyuan He
• 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 (arXiv 2023)
Yuyan Bao, Guannan Wei, Oliver Bračevac, Tiark Rompf (pdf).

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