Soft Session Types (Long Version)
Ugo Dal Lago, Paolo Di Giamberardino

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Parallel Computing and Optimization Techniques · Formal Methods in Verification
