Session Type Systems based on Linear Logic: Classical versus Intuitionistic

循环证明作为会话类型进程：一种局部有效性条件

Circular Proofs as Session-Typed Processes: A Local Validity Condition

本文扩展了直觉主义线性逻辑与会话类型π演算的对应关系到带最小和最大不动点的子结构逻辑片段，提出一个局部且可判定的有效性准则来识别对应有效循环证明的互递归进程，并证明该准则比既有守护条件更严格但更适合作编程语言基础。

Soft Session Types (Long Version)

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.

Soft Session Types

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.

比较派生自线性逻辑的会话类型系统

Comparing Session Type Systems derived from Linear Logic

本文严格比较了由线性逻辑的经典与直觉主义表述派生出的并发会话类型系统，开发了涵盖两者的 $π\mathsf{ULL}$ 系统作为参考框架，并基于局部性原则和进程组合形式分析了其差异。

关于经典与直觉主义线性进程

Around Classical and Intuitionistic Linear Processes

本文通过从CLL到ILL的翻译，基于类型化观察等价性，以完全抽象结果回答了经典与直觉主义线性逻辑并发类型系统之间的关系问题，揭示了它们之间缺失的形式化联系。