Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf

TL;DR

A flow-sensitive effect system for reachability types that supports explicit memory management, including Rust-style move semantics, in higher-order impure functional languages and formalizes the calculus, its typing and effect rules, and a compositional operational semantics that validates use-after-free safety.

Abstract

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} effects that record how references are read, written, transferred, and deallocated. The effect discipline tracks operations performed on each resource using qualifiers, enabling the type system to express ownership transfer, contextual freshness, and destructive updates without regions or linearity. We formalize the calculus, its typing and effect rules, and a compositional operational semantics that validates use-after-free safety. All metatheoretic results, including preservation, progress, and effect soundness, are mechanized. The system models idioms such as reference deallocation, move semantics, reference swapping, while exposing precise safety guarantee. Together, these contributions integrate reachability-based reasoning with explicit resource control, advancing the state of the art in safe manual memory management for higher-order functional languages.

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

TL;DR

A flow-sensitive effect system for reachability types that supports explicit memory management, including Rust-style move semantics, in higher-order impure functional languages and formalizes the calculus, its typing and effect rules, and a compositional operational semantics that validates use-after-free safety.

Abstract

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} effects that record how references are read, written, transferred, and deallocated. The effect discipline tracks operations performed on each resource using qualifiers, enabling the type system to express ownership transfer, contextual freshness, and destructive updates without regions or linearity. We formalize the calculus, its typing and effect rules, and a compositional operational semantics that validates use-after-free safety. All metatheoretic results, including preservation, progress, and effect soundness, are mechanized. The system models idioms such as reference deallocation, move semantics, reference swapping, while exposing precise safety guarantee. Together, these contributions integrate reachability-based reasoning with explicit resource control, advancing the state of the art in safe manual memory management for higher-order functional languages.

Paper Structure

This paper contains 59 sections, 1 theorem, 9 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Contributions
  3. Summary
  4. Reachability Types (RT)
  5. Key Ideas of RT
  6. Reachability Qualifiers: Tracking Reachable Resources in Types
  7. Freshness Marker in Function Arguments: Contextual Freshness
  8. Reference Type: Mutable Cells
  9. Extending RT with Effects
  10. Effects: Tracking Reads, Writes, Deallocation, and Ownership Transfer
  11. Use Effects for Reads and Writes
  12. Kill Effects for Deallocation
  13. Main Invariant: No Use-After-Kill
  14. Use vs. Mention
  15. Precise Effect Tracking
  16. ...and 44 more sections

Key Result

theorem 1

$\Sigma\mid \varnothing$$\,\vdash\,$t : $\ifenv{lstlisting}{\texttt{T}}{T}$${\color{eff}\varepsilon}$ σ∣ t $\mathrel{\longrightarrow}$ σ' ∣ t' $\Sigma\mid \varnothing\ \mathsf{ok}$$\Sigma\mid \varnothing$∣ k $\,\vdash\,$σ $\Gamma$⊢${\color{eff}\{\mathscr{k}: k\}}$$\mathbin{{\color{eff}\rhd}}$${\c

Figures (5)

  • Figure 1: The syntax of $\mathsf{F}_{\varepsilon <:}^{\vardiamondsuit}$.
  • Figure 2: Selected Typing rules of $\mathsf{F}_{\varepsilon <:}^{\vardiamondsuit}$. We omit cyclic reference types and dual-component reference types from deng_complete_2025 for simplicity. New constructs and additional typing constraints from deng_complete_2025 are $\colorbox{gray!20}{$\text{highlighted}$}$.
  • Figure 3: Subtyping rules of $\mathsf{F}_{\varepsilon <:}^{\vardiamondsuit}$.
  • Figure 4: Store Typing, Well-Formed Stores, and Operational Semantics for $\mathsf{F}_{\varepsilon <:}^{\vardiamondsuit}$. The semantics for free and move are highlighted in $\colorbox{gray!20}{$\text{gray boxes}$}$.
  • Figure 5: Operations on effects. Sequential effect composition is the component-wise set union and partial. It is only defined if no variable/location is used after being killed.

Theorems & Definitions (1)

  • theorem 1: Preservation