一句话：用逻辑关系为可达性类型建立语义模型，统一证明语义类型健全性、终止性、效应安全与程序等价。
可达性类型（reachability types）将 Rust 式内存性质推理引入高阶语言，支持高阶函数、参数化类型与共享可变状态，但已有工作仅用 progress/preservation 等语法方法建立类型健全性，更强元理论性质尚未探索。本文提出基于逻辑关系的语义模型，研究四类性质：(1) 语义类型健全性，包括对语法上非良类型代码片段；(2) 终止性，尤其在高阶可变引用下；(3) 效应安全性，尤其无可观测变异；(4) 程序等价性，尤其是非干扰表达式重排，以支持并行化或编译器优化。该语义框架为可达性类型提供了统一、可组合的推理基础。
Reachability types are a recent proposal to bring Rust-style reasoning about memory properties to higher-level languages, with a focus on higher-order functions, parametric types, and shared mutable state - features that are only partially supported by current techniques as employed in Rust. While prior work has established key type soundness results for reachability types using the usual syntactic techniques of progress and preservation, stronger metatheoretic properties have so far been unexplored. This paper presents an alternative semantic model of reachability types using logical relations, providing a framework in which we study key properties of interest: (1) semantic type soundness, including of not syntactically well-typed code fragments, (2) termination, especially in the presence of higher-order mutable references, (3) effect safety, especially the absence of observable mutation, and, finally, (4) program equivalence, especially reordering of non-interfering expressions for parallelization or compiler optimization.
@article{paperbot2918,
title = {Modeling Reachability Types with Logical Relations: Semantic Type Soundness, Termination, Effect Safety, and Equational Theory},
author = {Yuyan Bao and Songlin Jia and Guannan Wei and Oliver Bračevac and Tiark Rompf},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763116}
}