关联函数式与命令式会话类型
Relating Functional and Imperative Session Types
AI总结：
本文通过构造保持类型与语义的翻译，证明函数式会话类型包含命令式会话类型，并指出后者表达力不足主要源于其类型系统限制。
摘要：
命令式会话类型为会话类型化通信提供了一种命令式接口。在这种接口中，通道引用是一等对象，其操作会改变通道的类型状态。与函数式会话类型API相比，程序结构在表面上更简单，但全程需要类型状态来建模通信的当前状态。继一项探索命令式方法的早期工作之后，大量关于会话类型的研究忽视了命令式方法，转而采用利用线性类型来安全管理通道引用的函数式方法。我们通过展示一种保持类型和语义的翻译，将函数式方法归约为线性函数式会话类型系统，从而证明函数式方法包含了早期关于命令式会话类型的工作。我们进一步表明，从函数式演算到命令式演算的无类型反向翻译是保持语义的。我们限制函数式演算的类型系统，使得反向翻译成为保持类型的。因此，我们精确地捕捉了两种演算在表达能力上的差异，并得出结论：命令式演算缺乏表达能力，很大程度上是由于其类型系统施加的限制所致。
英文摘要：
Imperative session types provide an imperative interface to session-typed communication. In such an interface, channel references are first-class objects with operations that change the typestate of the channel. Compared to functional session type APIs, the program structure is simpler at the surface, but typestate is required to model the current state of communication throughout. Following an early work that explored the imperative approach, a significant body of work on session types has neglected the imperative approach and opts for a functional approach that uses linear types to manage channel references soundly. We demonstrate that the functional approach subsumes the early work on imperative session types by exhibiting a typing and semantics preserving translation into a system of linear functional session types. We further show that the untyped backwards translation from the functional to the imperative calculus is semantics preserving. We restrict the type system of the functional calculus such that the backwards translation becomes type preserving. Thus, we precisely capture the difference in expressiveness of the two calculi and conclude that the lack of expressiveness in the imperative calculus is largely due to restrictions imposed by its type system.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
