Soft Session Types


Paolo Di Giamberardino, Ugo Dal Lago

Proceedings 18th International Workshop on Expressiveness in Concurrency (EXPRESS) 64:59-73



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.