/reachability

Primary LanguageCoq

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

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).