freely 可移动：带流动敏感效应的可达性类型实现安全解除和所有权转移
编程语言
2025-10-13 v1
摘要
我们提出了一种用于可达性类型的流动敏感效应系统，支持更高阶纯函数语言中的显式内存管理，包括 Rust 风格的所有权语义。该系统细化了现有的可达性限定符，引入多态 \emph{use} 和 \emph{kill} 效应，用于记录引用的读取、写入、传输和解除方式。该效应体系使用限定符跟踪每个资源执行的操作，使类型系统能够在无需区域或线性代数的情况下表达所有权转移、上下文新鲜度和破坏性更新。我们形式化了微积分、其输入和效应规则，以及一种组合操作语义，该语义验证了 use-after-free 安全性。所有元理论结果，包括保存、进展和效应正确性，都被机械化。该系统模型了诸如引用解除、移动语义、引用交换等习惯用法，同时暴露了精确的安全保证。正是这些贡献将可达性推理与显式资源控制相结合，推动了更高阶函数语言中安全手动内存管理的前沿水平。
引用
@article{arxiv.2510.08939,
title = {Free to Move: Reachability Types with Flow-Sensitive Effects for Safe Deallocation and Ownership Transfer},
author = {Haotian Deng and Siyuan He and Songlin Jia and Yuyan Bao and Tiark Rompf},
journal= {arXiv preprint arXiv:2510.08939},
year = {2025}
}