具有协同规则的推理系统用于二元会话类型的组合安全性与活性性质
Inference Systems with Corules for Combined Safety and Liveness Properties of Binary Session Types
AI总结：
本文利用广义推理系统中的协同规则，为二元会话类型的组合安全性与活性性质（如公平终止、公平合规和公平子类型）提供更简单且完备的刻画，并借助有界余归纳原理证明其完备性。
摘要：
通信协议的许多性质结合了安全性与活性两个方面。由于定义和证明这些性质通常涉及根本不同的技术（分别是余归纳和归纳），通过单一推理系统来刻画此类组合性质是困难的。在本文中，我们表明广义推理系统使我们能够获得二元会话类型的这些组合归纳/余归纳性质（至少其中一些）的可靠且完备的刻画。特别地，我们阐述了协同规则在刻画公平终止（协议总能最终终止的性质）、公平合规（交互总能被扩展以达到客户端满足的性质）以及公平子类型（一种保持活性的会话类型细化关系）中的作用。我们获得的刻画与先前可用的刻画相比更为简单，并且协同规则为所确保或保持的活性性质提供了洞察。此外，我们可以方便地借助有界余归纳原理来证明所提供刻画的完备性。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
