一句话：首次将异步会话类型与异常处理集成到函数式语言，给出核心演算与 Links 实现。
会话类型可静态保证通信遵循协议，但多数会话类型系统不处理失败，因此在故障常见的真实应用尤其是分布式应用中用途有限。本文首次在函数式编程语言中形式化集成异步会话类型与异常处理。作者定义一个核心演算，证明其满足保持性与进展性，且无死锁、合流并终止。作者还通过扩展 Links Web 编程语言，给出首个面向成熟函数式语言的带异常处理会话类型实现，实现借鉴 effect handlers。评估包括双因素认证示例，以及一个更大的基于会话的聊天应用，其中通信通过会话类型化通道进行并能优雅处理断连。
Session types statically guarantee that communication complies with a protocol. However, most accounts of session typing do not account for failure, which means they are of limited use in real applications---especially distributed applications---where failure is pervasive. We present the first formal integration of asynchronous session types with exception handling in a functional programming language. We define a core calculus which satisfies preservation and progress properties, is deadlock free, confluent, and terminating. We provide the first implementation of session types with exception handling for a fully-fledged functional programming language, by extending the Links web programming language; our implementation draws on existing work on effect handlers. We illustrate our approach through a running example of two-factor authentication, and a larger example of a session-based chat application where communication occurs over session-typed channels and disconnections are handled gracefully.
@article{paperbot676,
title = {Exceptional asynchronous session types: session types without tiers},
author = {Simon Fowler and Sam Lindley and J. Garrett Morris and Sára Decova},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290341}
}