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.

翻译：静态资源管理在编程语言中仍然充满挑战，这源于控制力、表达能力和灵活性之间的张力。基于区域的系统[Grossman等人，2002；Tofte等人，2001]通过词法作用域区域提供批量释放机制，其中所有分配遵循栈式规则。然而，区域及其资源均为二等公民，既不能逃逸其作用域，也无法自由返回。以Rust为代表的拥有权和线性类型系统[Clarke等人，2013]提供了非词法生命周期和强大的静态保证，但其依赖的不变性限制了高阶模式和表达性共享。本文提出一种融合双方优势的新型类型系统。该系统将所有堆分配资源视为一等值，同时允许程序员通过三种分配模式控制生命周期和粒度：(1) 针对独立非词法引用的全新分配；(2) 在影子竞技场内进行后续协同分配以集体分组资源；(3) 遵循栈式规则的词法限定生命周期作用域分配。无论采用何种模式，所有资源共享统一类型，且对泛型抽象无差别处理，从而保持语言的高阶参数化特性。在支持灵活共享的高阶语言中实现静态安全性并非易事。我们通过扩展可达性类型[Wei等人，2024]来集体追踪一等资源，并采用流不敏感释放推理实现选择性栈规则，从而解决这一难题。这些机制催生了Aq<:与{A}q<:类型系统，两者均在Rocq中完成形式化验证，并证明具备类型安全性与内存安全性。