一句话：提出带 corules 的广义推理系统，统一刻画二元会话类型的组合安全性与活性性质，并给出可靠完备且更简单的刻画。
通信协议的性质常同时涉及安全性与活性，而两者通常分别依赖共归纳与归纳技术，难以由单一推理系统刻画。本文提出使用带 corules 的广义推理系统（Generalized Inference Systems）来统一处理二元会话类型的这类归纳/共归纳组合性质。作者以公平终止、公平合规与公平子类型为例，给出可靠且完备的刻画；这些刻画比已有工作更简单，corules 也揭示了被保证或保持的活性性质。完备性可借助有界共归纳原理证明。
Many properties of communication protocols combine safety and liveness aspects. Characterizing such combined properties by means of a single inference system is difficult because of the fundamentally different techniques (coinduction and induction, respectively) usually involved in defining and proving them. In this paper we show that Generalized Inference Systems allow us to obtain sound and complete characterizations of (at least some of) these combined inductive/coinductive properties of binary session types. In particular, we illustrate the role of corules in characterizing fair termination (the property of protocols that can always eventually terminate), fair compliance (the property of interactions that can always be extended to reach client satisfaction) and fair subtyping, a liveness-preserving refinement relation for session types. The characterizations we obtain are simpler compared to the previously available ones and corules provide insight on the liveness properties being ensured or preserved. Moreover, we can conveniently appeal to the bounded coinduction principle to prove the completeness of the provided characterizations.
@article{paperbot1659,
title = {Inference Systems with Corules for Combined Safety and Liveness Properties of Binary Session Types},
author = {Luca Ciccone and Luca Padovani},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 3},
year = {2022},
doi = {10.46298/lmcs-18(3:27)2022}
}