一句话：为高阶并发语言 IPA 建立多令牌 Petri 网机器，并用并发博弈证明其计算充分性。
本文研究 Idealized Parallel Algol（IPA）——一种带共享状态和信号量的高阶并发语言——的语义模型。作者提出一种多令牌机器，将项组合式地解释为 Petri 结构（着色 Petri 网）；在纯函数片段上，该机器与源自线性逻辑的交互几何（GoI）令牌机器相近，把高阶计算视为令牌在证明网中行走，同时结合一阶命令式并发程序到着色 Petri 网的表示。为证明机器相对于参考操作语义的计算充分性，作者采用博弈语义，将类型解释为规定计算事件之间依赖与冲突的博弈，并定义服从类型所抽取博弈规则的 Petri 策略。进一步，他们展示 Petri 策略可展开为事件结构上并发博弈意义下的并发策略。该联系不仅用于证明充分性，还能操作性地生成高阶类型程序行为的因果描述，并证明其与并发博弈指称解释一致。
We introduce a multi-token machine for Idealized Parallel Algol (IPA), a higher-order concurrent programming language with shared state and semaphores. Our machine takes the shape of a compositional interpretation of terms as Petri structures, certain coloured Petri nets. For the purely functional fragment of IPA, our machine is conceptually close to Geometry of Interaction token machines, originating from Linear Logic and presenting higher-order computation as the low-level process of a token walking through a graph (a proof net) representing the term. We combine here these ideas with folklore ideas on the representation of first-order imperative concurrent programs as coloured Petri nets. To prove our machine computationally adequate with respect to the reference operational semantics, we follow game semantics and represent types as certain games specifying dependencies and conflict between computational events. Petri strategies are those Petri structures obeying the rules of the game extracted from the type. We show how Petri strategies unfold to concurrent strategies in the sense of concurrent games on event structures. This link with concurrent strategies not only allows us to prove adequacy of our machine, but also lets us generate operationally a causal description of the behaviour of programs at higher-order types, which is shown to coincide with that given denotationally by the interpretation in concurrent games.
@article{paperbot2102,
title = {The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal Unfolding},
author = {Simon Castellan and Pierre Clairambault},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571217}
}