一句话：基于事件结构构造笛卡尔闭范畴 Cho，为高阶有状态并发程序给出精确且可组合的博弈语义。
本文为高阶有状态并发程序构造精细且可组合的语义。作者基于事件结构建立笛卡尔闭范畴 Cho，构造分两步：先建立紧致闭范畴 Tcg，作为 Rideau-Winskel 的 CG 的变体，为博弈与策略加入对称性以表达某些事件本质相同；再以 Hyland-Ong 博弈的标准 arena 为对象构造 Cho，其策略由事件结构表示，在 arena 展开形式诱导的对称博弈上运行。该语义组合地刻画执行，显式呈现因果依赖并记录非确定性分支点。Cho 解释纯函数式程序时对标准 Hyland-Ong 博弈与 innocent 策略保持保守，同时更具表达力；文中用 Cho 解释 Idealized Parallel Algol 的接近变体，提供操作视角。
We build a cartesian closed category, called Cho, based on event structures. It allows an interpretation of higher-order stateful concurrent programs that is refined and precise: on the one hand it is conservative with respect to standard Hyland-Ong games when interpreting purely functional programs as innocent strategies, while on the other hand it is much more expressive. The interpretation of programs constructs compositionally a representation of their execution that exhibits causal dependencies and remembers the points of non-deterministic branching.The construction is in two stages. First, we build a compact closed category Tcg. It is a variant of Rideau and Winskel's category CG, with the difference that games and strategies in Tcg are equipped with symmetry to express that certain events are essentially the same. This is analogous to the underlying category of AJM games enriching simple games with an equivalence relations on plays. Building on this category, we construct the cartesian closed category Cho as having as objects the standard arenas of Hyland-Ong games, with strategies, represented by certain events structures, playing on games with symmetry obtained as expanded forms of these arenas.To illustrate and give an operational light on these constructions, we interpret (a close variant of) Idealized Parallel Algol in Cho.
@article{paperbot822,
title = {Thin Games with Symmetry and Concurrent Hyland-Ong Games},
author = {Simon Castellan and Pierre Clairambault and Glynn Winskel},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 1},
year = {2019},
doi = {10.23638/lmcs-15(1:18)2019}
}