软会话类型（长版本）
Soft Session Types (Long Version)
摘要：
我们展示了如何系统的会话类型可以强制执行的所有类型的进程的相互作用是有界的。我们提出的类型系统是基于Lafont的软线性逻辑，并强烈的灵感来自最近的作品会话类型的直觉线性逻辑公式。我们的主要结果是存在的，对于每一个类型化的过程，一个多项式约束的长度上的任何减少序列从它开始，其任何减少的大小。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
