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.

翻译：本文提出一种流敏感的可达性类型效应系统，用于支持高阶非纯函数式语言中的显式内存管理（包括Rust风格的移动语义）。该系统通过多态的**使用**与**销毁**效应来精化现有的可达性限定符，这些效应记录了引用被读取、写入、转移和释放的过程。效应规则通过限定符追踪对每个资源执行的操作，使类型系统能够在不依赖区域或线性类型的情况下表达所有权转移、上下文新鲜性和破坏性更新。我们形式化了演算规则、类型与效应规则，以及验证释放后使用安全性的组合操作语义。所有元理论结果（包括保持性、进展性和效应可靠性）均已实现机械化验证。该系统建模了引用释放、移动语义、引用交换等编程范式，同时提供了精确的安全性保证。这些贡献共同将基于可达性的推理与显式资源控制相结合，推动了高阶函数式语言安全手动内存管理领域的技术发展。