We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

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

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 $\mu$MALL$^\infty$, 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 $\pi$LIN, a variant of the linear $\pi$-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 $\pi$LIN (and indirectly for session calculi through their encoding into $\pi$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.
Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)
Cite as: arXiv:2207.03749 [cs.LO]
  (or arXiv:2207.03749v1 [cs.LO] for this version)

Submission history

From: Luca Padovani [view email]
[v1] Fri, 8 Jul 2022 08:34:29 GMT (180kb,D)

Link back to: arXiv, form interface, contact.