Soft Session Types

Ugo Dal Lago
Paolo Di Giamberardino

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.

In Bas Luttik and Frank Valencia: Proceedings 18th International Workshop on Expressiveness in Concurrency (EXPRESS 2011), Aachen, Germany, 5th September 2011, Electronic Proceedings in Theoretical Computer Science 64, pp. 59–73.
Published: 20th August 2011.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: