paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Affine Sessions

仿射会话类型
LMCS vol.Volume 14, Issue 42018匹配度 2/10 · 论文研究会话类型、仿射性与并发错误处理,属于形式化类型系统与并发理论,与用户关注的 PL↔AI、LLM 辅助静态分析/形式化验证、浮点程序分析及贝叶斯程序分析等方向没有直接关联。引用 1 inbox
Dimitris Mostrous, Vasco T. Vasconcelos
crossref: 2026-09-10

AI 速览

一句话:将会话类型的线性约束放宽为仿射性,引入优雅错误处理并保持会话不会卡死的进展性。

会话类型通过线性来保证并发环境下通道严格按类型规定的顺序通信,避免干扰。本文把线性约束放宽为仿射性:通道至多执行类型规定的行为,而非必须完整执行。这个更宽松的设定使语言可以自然集成一种优雅的错误处理机制,相较已有基于异常的工作更简洁且有所改进。作者在保留会话类型核心保证的同时考察其与异常、错误终止的交互,并证明该处理不会损害语言的进展性质:会话不会卡死。

问题
如何在支持会话类型与并发通信的语言中放宽线性约束,以支持错误处理,同时不破坏通道行为保证和进展性。
方法
将线性会话类型改为仿射会话类型,允许通道至多完成其类型规定的行为,并据此设计错误/异常处理机制。
评估
通过理论论证表明,仿射放宽以及配套的错误处理不会影响语言的进展性质,即会话不会卡死。
原文摘要(Abstract)

Session types describe the structure of communications implemented by channels. In particular, they prescribe the sequence of communications, whether they are input or output actions, and the type of value exchanged. Crucial to any language with session types is the notion of linearity, which is essential to ensure that channels exhibit the behaviour prescribed by their type without interference in the presence of concurrency. In this work we relax the condition of linearity to that of affinity, by which channels exhibit at most the behaviour prescribed by their types. This more liberal setting allows us to incorporate an elegant error handling mechanism which simplifies and improves related works on exceptions. Moreover, our treatment does not affect the progress properties of the language: sessions never get stuck.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot358,
  title = {Affine Sessions},
  author = {Dimitris Mostrous and Vasco T. Vasconcelos},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 14, Issue 4},
  year = {2018},
  doi = {10.23638/lmcs-14(4:14)2018}
}