一句话：为 π 演算构建层语义模型，并证明其对公平测试等价是内涵全抽象的。
本文延续 CCS 的层语义工作，为 π 演算提出组合式模型：进程被解释为某些简单 site 上的层，这些层可视为 Hyland-Ong/Nickau 博弈语义中 innocent strategy 的并发形式。作者在模型中定义了公平测试等价的对应概念，并证明该解释相对于它满足内涵全抽象，即既保持又反映公平测试等价；同时任意 innocent strategy 都与某个进程的解释公平测试等价。工作的核心在于构造这些 site，其依赖 π 演算迹的组合式表示，并采用字符串图（string diagram）风格。
Following previous work on CCS, we propose a compositional model for the $\pi$-calculus in which processes are interpreted as sheaves on certain simple sites. Such sheaves are a concurrent form of innocent strategies, in the sense of Hyland-Ong/Nickau game semantics. We define an analogue of fair testing equivalence in the model and show that our interpretation is intensionally fully abstract for it. That is, the interpretation preserves and reflects fair testing equivalence; and furthermore, any innocent strategy is fair testing equivalent to the interpretation of some process. The central part of our work is the construction of our sites, relying on a combinatorial presentation of $\pi$-calculus traces in the spirit of string diagrams.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-1710-06744,
title = {An intensionally fully-abstract sheaf model for $\pi$ (expanded version)},
author = {Clovis Eberhart and Tom Hirschowitz and Thomas Seiller},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 4},
year = {2017},
doi = {10.23638/lmcs-13(4:9)2017}
}