论文标题
多方会议的公平终止
Fair Termination of Multiparty Sessions
论文作者
论文摘要
存在一个广泛的多方会议家庭，其中一个会话参与者的进度不是无条件的，而是取决于其他参与者的选择。这些会话不在当前可用的会话类型系统的范围之内，这些系统可以保证进度。在这项工作中，我们提出了第一种类型的系统，以确保良好的多党会议，包括表现出上述依赖关系的系统，相当终止。公平终止是在公平假设下终止的，该假设无视那些被认为是不公平的互动，因此是不现实的。公平终止，结合了在会话中确保的通常的安全性能，不仅本身是理想的，而且需要进步并实现静态分析的组成形式，从而使相当终止的会话的良好型组成导致相当终止的程序。
There exists a broad family of multiparty sessions in which the progress of one session participant is not unconditional, but depends on the choices performed by other participants. These sessions fall outside the scope of currently available session type systems that guarantee progress. In this work we propose the first type system ensuring that well-typed multiparty sessions, including those exhibiting the aforementioned dependencies, fairly terminate. Fair termination is termination under a fairness assumption that disregards those interactions deemed unfair and therefore unrealistic. Fair termination, combined with the usual safety properties ensured within sessions, not only is desirable per se, but it entails progress and enables a compositional form of static analysis such that the well-typed composition of fairly terminating sessions results in a fairly terminating program.
