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.
-
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. -
lr-- Logical relations for proving semantic type soundness of the$λ^*$ -calculus [1,3].
The mechanizations based on sets reuse some libraries by the UPenn PL Club that complement the FSet library shipping with Coq. We set up the FSet library with extensional equality as inspired by Boruch-Gruszecki et al.'s artifact.
-
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].
- Oliver Bračevac (Mechanization lead)
- Guannan Wei
- Yuyan Bao
- Siyuan He
- David Deng
- Tiark Rompf
[1] Reachability Types: Tracking Aliasing and Separation in Higher-order Functional Programs (OOPSLA 2021)
by Yuyan Bao, Guannan Wei, Oliver Bračevac, Luke Jiang, Qiyang He, and Tiark Rompf
(pdf).
[2] Polymorphic Reachability Types: Tracking Aliasing and Separation in Higher-order Generic Programs (2023)
by Guannan Wei, Oliver Bračevac, Siyuan He, Yuyan Bao, and Tiark Rompf
(to appear).
[3] Graph IRs for Impure Higher-Order Languages -- Making Aggressive Optimizations Affordable with Precise Effect Dependencies (OOPSLA 2023)
by Oliver Bračevac, Guannan Wei, Luke Jiang, Supun Abeysinghe, Songlin Jia, Siyuan He, Yuyan Bao, and Tiark Rompf
(to appear).