Soft Session Types (Long Version)
classification
💻 cs.LO
cs.PL
keywords
typeslinearlogicsessionsofttypableboundbounded
pith:HC34LL2R Add to your LaTeX paper
What is a Pith Number?\usepackage{pith}
\pithnumber{HC34LL2R}
Prints a linked pith:HC34LL2R badge after your title and writes the identifier into PDF metadata. Compiles on arXiv with no extra files. Learn more
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.