paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Distributed programming using role-parametric session types in go: statically-typed endpoint APIs for dynamically-instantiated communication structures

在 Go 中使用角色参数化会话类型进行分布式编程:面向动态实例化通信结构的静态类型端点 API
POPL 3(POPL)2019匹配度 2/10 · 论文属于纯 PL/类型系统方向,研究角色参数化多体会话类型与 Go 静态类型 API,未涉及 LLM/Agent、机器学习系统静态分析、浮点程序分析或贝叶斯程序分析。其形式化与工程实现虽符合偏好,但与用户当前核心研究画像交集很小。引用 55 inbox
David Castro, Raymond Hu, Sung-Shik Jongmans, Nicholas Ng, Nobuko Yoshida
crossref: 2026-09-10

AI 速览

一句话:提出角色参数化多体会话类型理论,并为 Go 生成静态类型端点 API,以安全实现动态参与者协议。

论文研究参与者数量与种类动态实例化的消息传递协议的安全编程。作者提出首个支持带索引角色的参数化协议的分布式多体会话类型(MPST)理论:静态推断协议诱导的角色变体,并将协议解耦投影到各变体,使分布式端点可由不同程序员、技术或语言独立实现。作者证明角色变体推断与良构性检查可判定、投影正确,并实现 Go 工具链,生成协议与变体专用的轻量类型包装 API 族;经原生 Go 类型检查的端点程序只执行符合源协议的 I/O。该框架支持多通道、混合传输与通道传递,并用微基准和真实应用评估适用性与运行时性能。

问题
当消息传递协议中参与者的数量和种类可动态实例化时,如何静态规定并安全实现协议。
方法
提出支持索引角色的参数化分布式多体会话类型(MPST),静态推断角色变体并生成各变体的端点投影,再为 Go 生成类型包装 API 族以约束端点 I/O。
评估
证明角色变体推断与良构性检查的可判定性及投影正确性;用微基准和真实应用评估生成 API 的适用性与运行时性能。
原文摘要(Abstract)

This paper presents a framework for the static specification and safe programming of message passing protocols where the number and kinds of participants are dynamically instantiated. We develop the first theory of distributed multiparty session types (MPST) to support parameterised protocols with indexed roles—our framework statically infers the different kinds of participants induced by a protocol definition as role variants, and produces decoupled endpoint projections of the protocol onto each variant. This enables safe MPST-based programming of the parameterised endpoints in distributed settings: each endpoint can be implemented separately by different programmers, using different techniques (or languages). We prove the decidability of role variant inference and well-formedness checking, and the correctness of projection. We implement our theory as a toolchain for programming such role-parametric MPST protocols in Go. Our approach is to generate API families of lightweight, protocol- and variant-specific type wrappers for I/O. The APIs ensure a well-typed Go endpoint program (by native Go type checking) will perform only compliant I/O actions w.r.t. the source protocol. We leverage the abstractions of MPST to support the specification and implementation of Go applications involving multiple channels, possibly over mixed transports (e.g., Go channels, TCP), and channel passing via a unified programming interface. We evaluate the applicability and run-time performance of our generated APIs using microbenchmarks and real-world applications.

链接与引用

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

BibTeX
@article{paperbot633,
  title = {Distributed programming using role-parametric session types in go: statically-typed endpoint APIs for dynamically-instantiated communication structures},
  author = {David Castro and Raymond Hu and Sung-Shik Jongmans and Nicholas Ng and Nobuko Yoshida},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {3},
  number = {POPL},
  year = {2019},
  doi = {10.1145/3290342}
}