一句话：为Mazza多端口交互组合子提出多令牌几何交互模型，并证明其可靠性与充分性。
本文研究如何为Mazza的多端口交互组合子提供语义模型。该组合子是图论式形式系统，能够忠实刻画π演算等进程代数所体现的并发计算。作者引入一种几何交互（geometry of interaction）模型，其核心是基于令牌机的机制：并非只有一个令牌，而是允许多个令牌同时遍历底层交互网，从而自然处理多端口交互。论文证明该模型的可靠性与充分性：可靠性通过任意归约序列上所得令牌机之间的模拟关系建立，充分性则依赖对交互网与令牌机中收敛性的精细分析。该工作将几何交互方法拓展到并发交互场景，为并发进程的语义刻画提供了新的机器模型。
We introduce a geometry of interaction model for Mazza's multiport interaction combinators, a graph-theoretic formalism which is able to faithfully capture concurrent computation as embodied by process algebras like the π-calculus. The introduced model is based on token machines in which not one but multiple tokens are allowed to traverse the underlying net at the same time. We prove soundness and adequacy of the introduced model. The former is proved as a simulation result between the token machines one obtains along any reduction sequence. The latter is obtained by a fine analysis of convergence, both in nets and in token machines.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{LagoTY17,
title = {The geometry of concurrent interaction: Handling multiple ports by way of multiple tokens},
author = {Ugo Dal Lago and Ryo Tanaka and Akira Yoshimizu},
booktitle = {LICS},
year = {2017},
doi = {10.1109/lics.2017.8005112}
}