License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ICALP.2021.125
URN: urn:nbn:de:0030-drops-141941
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14194/
Ciccone, Luca ;
Padovani, Luca
Inference Systems with Corules for Fair Subtyping and Liveness Properties of Binary Session Types
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.
BibTeX - Entry
@InProceedings{ciccone_et_al:LIPIcs.ICALP.2021.125,
author = {Ciccone, Luca and Padovani, Luca},
title = {{Inference Systems with Corules for Fair Subtyping and Liveness Properties of Binary Session Types}},
booktitle = {48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
pages = {125:1--125:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-195-5},
ISSN = {1868-8969},
year = {2021},
volume = {198},
editor = {Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/14194},
URN = {urn:nbn:de:0030-drops-141941},
doi = {10.4230/LIPIcs.ICALP.2021.125},
annote = {Keywords: Inference systems, session types, safety, liveness, induction, coinduction}
}
