Reachability types are a recent proposal to bring Rust-style reasoning about memory properties to higher-level languages. While key type soundness results for reachability types have been established using syntactic techniques in prior work, 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 to study key properties of interest such as (1) semantic type soundness, including of not syntactically well-typed code fragments, (2) termination, especially in the presence of higher-order state, and (3) program equivalence, especially reordering of non-interfering expressions for parallelization or compiler optimization.

翻译：可达类型是近期提出的一种将Rust风格的内存属性推理推广至高级语言的方法。尽管先前的研究已通过语法技术确立了可达类型的关键类型可靠性结果，但更强的元理论性质至今尚未被探索。本文提出了一种基于逻辑关系的可达类型语义模型，为研究以下关键性质提供了一个框架：(1) 语义类型可靠性，包括对非语法良类型的代码片段；(2) 终止性，特别是在存在高阶状态的情况下；(3) 程序等价性，特别是对无干扰表达式进行重排序以支持并行化或编译器优化。