Soft Session Types

TL;DR

This paper introduces a session type system based on soft linear logic that guarantees polynomial bounds on interaction lengths and process sizes, enhancing the analysis of process interactions.

Contribution

It proposes a novel soft session type system inspired by Lafont's soft linear logic, providing polynomial bounds for all typable processes.

Findings

Polynomial bounds on reduction sequences

Bounded interaction lengths for typable processes

Size constraints on process reducts

Abstract

We show how systems of session types can enforce interactions to be bounded for all typable processes. The type system we propose is based on Lafont's soft linear logic and is strongly inspired by recent works about session types as intuitionistic linear logic formulas. Our main result is the existence, for every typable process, of a polynomial bound on the length of any reduction sequence starting from it and on the size of any of its reducts.