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

Abstract: Session types describe the communication behavior of interacting processes. Binary session types are a particular form of session types in which each channel has two endpoints. The strong progress property states that a recursive process either terminates or communicates along one of its external channels after a finite number of steps. In this talk, I show how to prove strong progress for valid session-typed processes defined in an asynchronous computational semantics, working in a fragment of binary session types in which a process can use at most one resource. We formalize a proof of strong progress via a processes-as-formulas interpretation into a metalogic that we have introduced. The metalogic is an infinitary first order linear calculus with least and greatest fixed-points. We build a circular derivation for the strong progress property of processes in this first order calculus. By enforcing a condition on the logical derivations, we ensure their cut elimination property and soundness of the strong progress theorem.

logic in computer sciencelogic

Audience: researchers in the topic

Online logic seminar

Series comments: Description: Seminar on all areas of logic