Inference Systems with Corules for Fair Subtyping and Liveness Properties of Binary Session Types
Contributo in Atti di convegno
Data di Pubblicazione:
2021
Abstract:
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.
Tipologia CRIS:
04A-Conference paper in volume
Keywords:
Inference systems, session types, safety, liveness, induction, coinduction
Elenco autori:
Luca Ciccone; Luca Padovani
Link alla scheda completa:
Link al Full Text:
Titolo del libro:
Proceedings of the 48th International Colloquium on Automata, Languages, and Programming (ICALP’21)
Pubblicato in: