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