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.CONCUR.2022.36
URN: urn:nbn:de:0030-drops-170990
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/17099/
Go to the corresponding LIPIcs Volume Portal

Ciccone, Luca ; Padovani, Luca

An Infinitary Proof Theory of Linear Logic Ensuring Fair Termination in the Linear π-Calculus

pdf-format:
LIPIcs-CONCUR-2022-36.pdf (0.8 MB)

Abstract

Fair termination is the property of programs that may diverge "in principle" but that terminate "in practice", i.e. under suitable fairness assumptions concerning the resolution of non-deterministic choices. We study a conservative extension of μMALL^∞, the infinitary proof system of the multiplicative additive fragment of linear logic with least and greatest fixed points, such that cut elimination corresponds to fair termination. Proof terms are processes of πLIN, a variant of the linear π-calculus with (co)recursive types into which binary and (some) multiparty sessions can be encoded. As a result we obtain a behavioral type system for πLIN (and indirectly for session calculi through their encoding into πLIN) that ensures fair termination: although well-typed processes may engage in arbitrarily long interactions, they are fairly guaranteed to eventually perform all pending actions.

BibTeX - Entry

@InProceedings{ciccone_et_al:LIPIcs.CONCUR.2022.36,
  author =	{Ciccone, Luca and Padovani, Luca},
  title =	{{An Infinitary Proof Theory of Linear Logic Ensuring Fair Termination in the Linear \pi-Calculus}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{36:1--36:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/17099},
  URN =		{urn:nbn:de:0030-drops-170990},
  doi =		{10.4230/LIPIcs.CONCUR.2022.36},
  annote =	{Keywords: Linear \pi-calculus, Linear Logic, Fixed Points, Fair Termination}
}

Keywords: Linear π-calculus, Linear Logic, Fixed Points, Fair Termination
Collection: 33rd International Conference on Concurrency Theory (CONCUR 2022)
Issue Date: 2022
Date of publication: 06.09.2022

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