一句话：首次为可达性类型建立可靠迹模型并精化为完全抽象语义，并给出情境近似结果。
可达性类型通过类型化保证高阶语言中的分离性，但其情境等价问题因可达性约束限制上下文可观察的交互（尤其顺序性）而变复杂。本文从操作博弈语义视角研究可达性类型的情境等价：先给出一个可靠的迹模型，再将其精化为完全抽象模型，该模型基于在遵守可达性注解的前提下允许项一致共享函数与位置的等价。文章还讨论情境近似，并给出不等式形式的完全抽象结果。这是首个为可达性类型定义完全抽象语义的尝试。
Reachability types are a recent approach to modelling sharing in higher-order languages, aiming to provide separation guarantees through typability. The contextual equivalence problem in such a setting is exacerbated by the need to consider reachability-related constraints on the allowable interactions. In particular, they might weaken the ability of contexts to observe sequentiality.In this paper, we investigate contextual equivalence for reach-ability types through the lens of operational game semantics. We provide a sound trace model for a language equipped with reachability types, and show how to refine it to a fully abstract one, which captures a natural notion of equivalence based on allowing terms to share functions and locations consistently with the assigned reachability annotations. We also discuss the corresponding problem of contextual approximation, along with an inequational full abstraction result.This is a first attempt at defining a fully abstract semantics for reachability types.
DOI 原文 ·
@inproceedings{paperbot8622,
title = {Reachability Types, Traces and Full Abstraction},
author = {Benedict Bunting and Andrzej S. Murawski},
booktitle = {LICS},
year = {2025},
doi = {10.1109/lics65433.2025.00046}
}