First-order store and visibility in name-passing calculi
计算机科学中的逻辑
2025-04-25 v1
摘要
-calculus是典型的名称传递计算方法。虽然它纯粹基于名称传递，却允许表示更高阶函数和存储。我们研究如何控制-计算过程，使计算仅涉及一级值的存储。该纪律通过基于游戏语义中可见性概念的类型系统强制实施。我们讨论了可见性对行为理论的影响。我们提出了基于（变量的）迹等价性和标记双线性相似性的 may-testing 和 barbed equivalence 的表征，在计算顺序情况下以及计算良好括号化的情况下。
引用
@article{arxiv.2504.17350,
title = {First-order store and visibility in name-passing calculi},
author = {Daniel Hirschkoff and Iwan Quémerais and Davide Sangiorgi},
journal= {arXiv preprint arXiv:2504.17350},
year = {2025}
}