一句话：提出基于借用的会话类型 API 与 BGV 演算，用有序线性类型和到 PGV 的翻译保证类型安全与无死锁。
传统函数式会话类型系统把通道作为一等值，其 API 在处理模块性与可组合性时常常带来冗余限制。本文提出一种基于 borrowing（借用）的会话类型 API，并形式化为核心演算 BGV。该演算建立在有序线性类型之上，提供显式的通道所有权分割操作，使会话类型客户端代码更模块化、可组合。为奠定语义，作者给出从 BGV 到无死锁函数式会话类型演算 PGV 的类型保持翻译，并由此证明 BGV 的类型安全与死锁自由。论文还给出支持借用记法的外部语言版本，开发了算法化类型系统，并机器验证从外部语言到 BGV 的翻译，从而确立可判定类型检查。
Session types provide a formal framework to enforce rich communication protocols, ensuring correctness properties such as type safety and deadlock freedom. However, the traditional API of functional session type systems with first-class channels often leads to problems with modularity and composability. This paper proposes a new, alternative session type API based on borrowing, embodied in the core calculus BGV. The borrowing-based API enables building modular and composable code for session type clients without imposing clutter or undue limitations. Its basis is a novel type system, founded on ordered linear typing, for functional session types with an explicit operation for splitting ownership of channels. We establish the semantics of BGV via a type-preserving translation to PGV, a deadlock-free functional session type calculus. We establish type safety and deadlock freedom for BGV by this translation. We also present an external version of BGV that supports use of borrow notation. We developed an algorithmic version of the type system that includes a mechanized verified translation from the external language to BGV. This part establishes decidable type checking.
@article{paperbot2928,
title = {Borrowing from Session Types},
author = {Hannes Saffrich and Janek Spaderna and Peter Thiemann and Vasco T. Vasconcelos},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763173}
}