Soft Session Types (Long Version)

Ugo Dal Lago; Paolo Di Giamberardino

Soft Session Types (Long Version)

Logic in Computer Science 2012-01-04 v3 Programming Languages

Authors: Ugo Dal Lago , Paolo Di Giamberardino

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.

Keywords

type theory process calculus algebraic theory

Cite

@article{arxiv.1107.4478,
  title  = {Soft Session Types (Long Version)},
  author = {Ugo Dal Lago and Paolo Di Giamberardino},
  journal= {arXiv preprint arXiv:1107.4478},
  year   = {2012}
}