Haotian Deng

Free to Move: Reachability Types with Flow-Sensitive Effects for Safe Deallocation and Ownership Transfer

2025 · arXiv (Cornell University)

We present a flow-sensitive effect system for reachability types that supports explicit memory management, including Rust-style move semantics, in higher-order impure functional languages. Our system refines the existing reachability qualifier with polymorphic \emph{use} and \emph{kill} …