On Session Types and Polynomial Time


Paolo Di Giamberardino, Ugo Dal Lago


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.
The type system we present here is a revised and simpler version of the one presented in our EXPRESS 2011 paper.