When Lifetimes Liberate: A Type System for Arenas with Higher-Order Reachability Tracking

TL;DR

This work addresses static resource management in higher-order languages by unifying region-like lifetime control with first-class heap resources, introducing three allocation modes and a two-dimensional arena-store model. It develops two calculi, $\mathsf{A}_{<:}^{\vardiamondsuit}$ for arena-based reachability tracking and ${\left\{\mathsf{A}\right\}}_{<:}^{\vardiamondsuit}$ for scoped resource management, combining coarse-grained arena reasoning with flow-insensitive deallocation. Reachability tracking is extended to shadow arenas to enable collective reasoning about resources within arenas, while scoped allocation provides guaranteed bulk deallocation without flow-sensitive analysis. The framework supports higher-order sharing, mutual recursion, and cyclic store structures, and is mechanized in Rocq with three concrete case studies (callbacks, fixed-point combinators, and multi-hop cycles). Overall, the paper delivers a unified, expressive, and memory-safe approach that reconciles first-class heap resources with controlled lifetimes, offering practical benefits for safe resource management in higher-order languages.

Abstract

Static resource management in languages remains challenging due to tensions among control, expressiveness, and flexibility. Region-based systems [Grossman et al . 2002; Tofte et al. 2001] offer bulk deallocation via lexically scoped regions, where all allocations follow a stack discipline. However, both regions and their resources are second-class, and neither can escape its scope nor be freely returned. Ownership and linear type systems, exemplified by Rust [Clarke et al. 2013], offer non-lexical lifetimes and robust static guarantees, but rely on invariants that limit higher-order patterns and expressive sharing. In this work, we propose a new type system that unifies these strengths. Our system treats all heap-allocated resources as first-class values, while allowing programmers to control lifetime and granularity through three allocation modes: (1) fresh allocation for individual, non-lexical references; (2) subsequent coallocation grouping resources collectively within shadow arenas; and (3) scoped allocation with lexically bounded lifetimes following stack discipline. Regardless of mode, all resources share a uniform type and have no distinction for generic abstractions, preserving the higher-order parametric nature of the language. Obtaining static safety in higher-order languages with flexible sharing is nontrivial. We address this by extending reachability types [Wei et al. 2024] to collectively track first-class resources, and by adopting flow-insensitive deallocation reasoning for selective stack discipline. These mechanisms yield Aq<: and {A}q<: atop, both formalized and proven type safe and memory safe in Rocq.

Figures (17)

• Figure 1: An allocation can take one of three forms: primitive (), scoped (), and coallocation (). Scoped arenas ( e.g., ) are deallocated when leaving the scope.
• Figure 2: The two dimensional layout produced by (a). Two arenas are created; they can be referred to in clauses through existing cells, e.g., .
• Figure 4: The comparison of store topology between Rust rust (left) and reachability type david (right). Circular nodes in purple represent store locations. Directed edges represent the references from one location to another, ruled by either ownership or reachability, respectively. The timeline indicates the order of allocation in the program flow.
• Figure 5: The store topology of this work (left) and illustration of cross-arena cycles (right). Arenas are marked as boxes containing multiple store locations filled with light orange. Internal reachability are marked in teal. Telescoping structures and exclusivity are relaxed in our work.
• Figure 6: The syntax of $\mathsf{A}_{<:}^{\vardiamondsuit}$. Extensions from wei24 and david are $\colorbox{pink!60}{$\text{shaded}$}$.

Theorems & Definitions (15)

• theorem 1: Progress
• theorem 2: Preservation
• theorem 3: Progress
• theorem 4: Preservation
• lemma 1: Observability
• lemma 2: Value Observability
• lemma 3: Value Retyping
• lemma 4: Values are Non-Fresh
• lemma 5: Well-Stepped Values
• lemma 6: Well-Stepping of Terms