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: https://drops.dagstuhl.de/opus/volltexte/2021/14194/
Go to the corresponding LIPIcs Volume Portal


Ciccone, Luca ; Padovani, Luca

Inference Systems with Corules for Fair Subtyping and Liveness Properties of Binary Session Types

pdf-format:
LIPIcs-ICALP-2021-125.pdf (0.7 MB)


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}
}

Keywords: Inference systems, session types, safety, liveness, induction, coinduction
Collection: 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)
Issue Date: 2021
Date of publication: 02.07.2021
Supplementary Material: The Agda formalization of the notions and results presented in the paper is available at
Model (Agda Formalization): https://github.com/boystrange/FairSubtypingAgda/tree/v1.0 archived at: https://archive.softwareheritage.org/swh:1:rev:6d00f452a8380c2aacc659b2a69b9f4b3accfa27


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI