文章基本信息

标题：Inference Systems with Corules for Fair Subtyping and Liveness Properties of Binary Session Types
本地全文：下载
作者：Ciccone, Luca ; Padovani, Luca
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2021
卷号：198
DOI：10.4230/LIPIcs.ICALP.2021.125
语种：English
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：Many properties of communication protocols stem from the combination of safety and liveness properties. 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 for simple and insightful characterizations of (at least some of) these combined inductive/coinductive properties for dependent session types. In particular, we illustrate the role of corules in characterizing weak 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 also fair subtyping, a liveness-preserving refinement relation for session types.
关键词：Inference systems;session types;safety;liveness;induction;coinduction