paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Parameterized Algebraic Protocols

参数化代数协议
PLDI 7(PLDI)2023匹配度 2/10 · 该论文主题是会话类型、代数协议与线性时间类型检查,属于类型系统与并发理论,与用户关注的 PL↔AI、LLM/Agent、浮点程序分析及贝叶斯程序分析无直接关联。仅在静态分析/类型检查的形式化方法上可能有间接参考价值。引用 4 inbox
Andreia Mordido, Janek Spaderna, Peter Thiemann, Vasco T. Vasconcelos
crossref: 2026-09-10

AI 速览

一句话:提出参数化代数协议,以代数数据类型风格统一并扩展会话类型,实现线性时间类型检查。

该论文提出参数化代数协议(parameterized algebraic protocols),使协议模板和会话类型能像代数数据类型定义领域特定类型那样被定义与组合。该形式涵盖所有正则会话类型以及大多数上下文无关与嵌套会话类型,用基于名义的线性时间检查替代传统超线性类型检查算法,从而提高可扩展性。结合多态后,代数协议进一步增强表达力与模块化,支持新的会话类型参数化与组合方式。作者通过形式化比较和复杂度分析论证其包容性与效率改进。

问题
会话类型在表达复杂协议时面临表达力受限或类型检查算法超线性开销大的问题,且难以像代数数据类型一样模板化、参数化与模块化复用。
方法
提出参数化代数协议,以代数数据类型风格定义协议模板和会话类型,并用名义检查实现线性时间类型检查,结合多态增强表达力与组合性。
评估
通过形式化分析将其与正则、上下文无关和嵌套会话类型比较,并分析类型检查复杂度,表明可涵盖后者且将超线性检查改进为线性。
原文摘要(Abstract)

We propose algebraic protocols that enable the definition of protocol templates and session types analogous to the definition of domain-specific types with algebraic datatypes. Parameterized algebraic protocols subsume all regular as well as most context-free and nested session types and, at the same time, replace the expensive superlinear algorithms for type checking by a nominal check that runs in linear time. Algebraic protocols in combination with polymorphism increase expressiveness and modularity by facilitating new ways of parameterizing and composing session types.

链接与引用

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

BibTeX
@article{paperbot1962,
  title = {Parameterized Algebraic Protocols},
  author = {Andreia Mordido and Janek Spaderna and Peter Thiemann and Vasco T. Vasconcelos},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {7},
  number = {PLDI},
  year = {2023},
  doi = {10.1145/3591277}
}