一句话：建立 λ-演算的 π-演算编码与操作博弈语义的紧密联系，证明二者诱导的等价一致并迁移多项结果。
论文研究 λ-演算的两种模型——Milner 将 λ-项编码到 π-演算（Internal π）与操作博弈语义（OGS）——之间的关系。作者针对多组 LTS 建立编码行为与 OGS 行为的操作对应：π 的标准 LTS 与 OGS 的新并发 LTS，π 的输出优先 LTS 与 OGS 的标准交替 LTS，并证明它们在 λ-项上诱导的等价一致。基于完整迹时，OGS 的并发、交替与良括号变体也一致。由此可在 π 与 OGS 间迁移结果：把 π 的 up-to 技术引入 OGS，从 π 推导 OGS 的同余与组合性，并把完整迹概念搬到 π，得到对带 store 的 λ-演算上下文的完全抽象。CBV/CBN 均适用。
We establish a tight connection between two models of the $λ$-calculus, namely Milner's encoding into the $π$-calculus (precisely, the Internal $π$-calculus), and operational game semantics (OGS). We first investigate the operational correspondence between the behaviours of the encoding provided by $π$ and OGS. We do so for various LTSs: the standard LTS for $π$ and a new `concurrent' LTS for OGS; an `output-prioritised' LTS for $π$ and the standard alternating LTS for OGS. We then show that the equivalences induced on $λ$-terms by all these LTSs (for $π$ and OGS) coincide. We also prove that when equivalence is based on complete traces, the `concurrent' and `alternating' variants of OGS also coincide with the `well-bracketed' variant. These connections allow us to transfer results and techniques between $π$ and OGS. In particular: we import up-to techniques from $π$ onto OGS; we derive congruence and compositionality results for OGS from those of $π$; we transport the notion of complete traces from OGS onto $π$, obtaining a new behavioural equivalence that yields a full abstraction result for the encoding of $λ$-terms with respect to contexts written in a $λ$-calculus extended with store. The study is illustrated for both call-by-value and call-by-name.
@article{paperbot12175,
title = {Games, mobile processes, and functionss -- alternating, concurrent, and well-bracketed semantics},
author = {Guilheme Jaber and Davide Sangiorgi},
journal = {Logical Methods in Computer Science},
volume = {Volume 22, Issue 4},
year = {2026},
doi = {10.46298/lmcs-22(4:2)2026}
}