Strong Progress for Session-Typed Processes in a Linear Metalogic with Circular Proofs

TL;DR

This paper presents a new infinitary linear logic framework with fixed points, enabling the proof of strong progress for session-typed processes, a novel result in asynchronous communication semantics.

Contribution

It introduces a linear logic with fixed points and circular proofs, and applies it to establish the first proof of strong progress for session-typed processes.

Findings

Proves strong progress property for session-typed processes

Develops a linear logic with fixed points and circular proofs

Ensures cut elimination with a validity condition

Abstract

We introduce an infinitary first order linear logic with least and greatest fixed points. To ensure cut elimination, we impose a validity condition on infinite derivations. Our calculus is designed to reason about rich signatures of mutually defined inductive and coinductive linear predicates. In a major case study we use it to prove the strong progress property for binary session-typed processes under an asynchronous communication semantics. As far as we are aware, this is the first proof of this property.