结合二元会话类型安全性与活性性质的共规则推理系统
计算机科学中的逻辑
2023-06-22 v4
摘要
通信协议的许多性质结合了安全性和活性两个方面。由于定义和证明这些性质通常涉及根本不同的技术（分别为余归纳和归纳），用单一推理系统来刻画这种组合性质是困难的。在本文中，我们证明了广义推理系统使我们能够获得二元会话类型的这些组合归纳/余归纳性质的可靠且完备的刻画（至少是其中一些）。特别地，我们阐述了共规则在刻画公平终止（协议总能最终终止的性质）、公平合规（交互总能扩展以达到客户端满意的性质）以及公平子类型（一种保持活性的会话类型细化关系）中的作用。我们获得的刻画比先前已有的刻画更简单，并且共规则为所确保或保持的活性性质提供了洞见。此外，我们可以方便地诉诸有界余归纳原理来证明所提供刻画的完备性。
引用
@article{arxiv.2108.01503,
title = {Inference Systems with Corules for Combined Safety and Liveness Properties of Binary Session Types},
author = {Luca Ciccone and Luca Padovani},
journal= {arXiv preprint arXiv:2108.01503},
year = {2023}
}