利用逻辑关系对可达性类型进行建模：语义类型正确性、终止性、效果安全性及等式理论

《Proceedings of the ACM on Programming Languages》：Modeling Reachability Types with Logical Relations: Semantic Type Soundness, Termination, Effect Safety, and Equational Theory

本文提出基于逻辑关系的可达性类型语义模型，解决现有技术在高阶函数和共享可变状态支持上的不足，验证类型正确性、终止性、效应安全及程序等价性。

　　

摘要

可达性类型是一种近期提出的方法，旨在将Rust风格的关于内存属性的推理机制引入到更高级的语言中，重点关注高阶函数、参数化类型以及共享的可变状态——这些特性在当前Rust中使用的技术中仅得到了部分支持。虽然之前的研究已经利用常规的“进展”和“保持”等语法技术证明了可达性类型的关键类型正确性，但更强的元理论属性至今尚未被探索。本文提出了一种基于逻辑关系的可达性类型的替代语义模型，为研究以下关键属性提供了框架：（1）语义类型正确性，包括那些在语法上并不完全符合类型要求的代码片段；（2）终止性，特别是在存在高阶可变引用的情况下；（3）效果安全性，尤其是不存在可观察到的状态变化；最后是（4）程序等价性，特别是为了并行化或编译器优化而对非相互干扰的表达式进行重新排序的情况。