一句话：提出可类型化所有异步多参与者会话的全局类型系统，并给出可靠完备的类型推断算法。
多参与者会话与全局类型可用于建模分布式系统中的交互协议，目标是通过类型系统保证所有参与者满足良好性质，同时最大化可接受行为。本文针对异步通信，提出一种“去禁闭”全局类型系统，能够为所有异步会话给出类型，改进了现有工作。在满足若干良构条件时，系统保持主体归约、会话保真与进展等关键性质。作者还给出可靠且完备的类型推断算法。由于良构条件本身不可判定，文中进一步设计算法检查其一个表达力较强的可判定限制，从而恢复类型化的有效性。
Multiparty sessions with asynchronous communications and global types play an important role for the modelling of interaction protocols in distributed systems. In designing such calculi the aim is to enforce, by typing, good properties for all participants, maximising, at the same time, the accepted behaviours. Our type system improves the state-of-the-art by typing all asynchronous sessions and preserving the key properties of Subject Reduction, Session Fidelity and Progress when some well-formedness conditions are satisfied. The type system comes together with a sound and complete type inference algorithm. The well-formedness conditions are undecidable, but an algorithm checking an expressive restriction of them recovers the effectiveness of typing.
@article{paperbot2247,
title = {Deconfined Global Types for Asynchronous Sessions},
author = {Francesco Dagnino and Paola Giannini and Mariangiola Dezani-Ciancaglini},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 1},
year = {2023},
doi = {10.46298/lmcs-19(1:3)2023}
}