Soft Session Types (Long Version)

TL;DR

This paper introduces a session type system based on soft linear logic that guarantees polynomial bounds on process interactions, ensuring bounded communication sequences for typable processes.

Contribution

It proposes a novel soft session type system inspired by Lafont's soft linear logic, providing polynomial bounds on process reduction lengths and sizes.

Findings

Every typable process has a polynomial bound on reduction length.

Reducts of typable processes are also polynomially bounded in size.

The system enforces interaction bounds for all typable processes.

Abstract

We show how systems of sessions 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.