Higher-order impure programs routinely transfer or consume a resource through a closure: when one access path consumes the resource, it must be disabled through all remaining aliases---including those captured in closures---precisely at the point of consumption. We present a flow-sensitive type-and-effect system for reachability types that makes such ownership transfer sound in the presence of higher-order control flow. The key idea is simple: every computation can induce a use and/or a kill effect. The system statically tracks them, rejects any use of a killed resource. With reachability qualifiers and flow-sensitive effects, the system also derives on-demand uniqueness patterns compatible with higher-order impure functions. We illustrate the practicality of the system through numerous case studies such as a freezable counter, a destructive merge on unique linked lists, Rust-style swap on Box, recursive sum on unique linked lists, and use-once continuations. We formalize the system as the $\mathsf{F}_{\varepsilon <:}^{\diamondsuit}$ calculus, present its typing rules and operational semantics, and prove effect soundness, including multi-step preservation and preservation under parallel reduction. We mechanize all key results in Rocq.

翻译：暂无翻译