English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Fair termination is the property of programs that may diverge "in principle"but that terminate "in practice", i.e. under suitable fairness assumptionsconcerning the resolution of non-deterministic choices. We study a conservativeextension of $\mu$MALL$^\infty$, the infinitary proof system of themultiplicative additive fragment of linear logic with least and greatest fixedpoints, such that cut elimination corresponds to fair termination. Proof termsare processes of $\pi$LIN, a variant of the linear $\pi$-calculus with(co)recursive types into which binary and (some) multiparty sessions can beencoded. As a result we obtain a behavioral type system for $\pi$LIN (andindirectly for session calculi through their encoding into $\pi$LIN) thatensures fair termination: although well-typed processes may engage inarbitrarily long interactions, they are fairly guaranteed to eventually performall pending actions.

An Infinitary Proof Theory of Linear Logic Ensuring Fair Termination in the Linear $\pi$-Calculus