一句话：提出 GradualGV，将动态类型与 cast 引入函数式会话类型系统 GV，统一静态与动态会话处理并保证类型、通信与 blame 安全。
Web 应用与微服务常混合使用静态和动态类型语言，而基于线性类型的会话类型虽能保证通信安全，却难以直接适应这种混合场景。本文提出 GradualGV，在函数式会话类型系统 GV 上扩展动态类型与 cast，使会话处理可在静态类型检查与任意程度的动态类型之间无缝过渡。由于线性与动态类型相互作用，论文给出新的语言动态语义。作者证明了类型安全、通信安全与 blame safety，将渐进类型与 blame 的既有结果推广到基于会话通信的函数式语言。
Session types are a rich type discipline, based on linear types, that lift the sort of safety claims that come with type systems to communications. However, web-based applications and micro services are often written in a mix of languages, with type disciplines in a spectrum between static and dynamic typing. Gradual session types address this mixed setting by providing a framework which grants seamless transition between statically typed handling of sessions and any required degree of dynamic typing. We propose GradualGV as an extension of the functional session type system GV with dynamic types and casts. We demonstrate type and communication safety as well as blame safety, thus extending previous results to functional languages with session-based communication. The interplay of linearity and dynamic types requires a novel approach to specifying the dynamics of the language.
@article{paperbot29,
title = {Gradual session types},
author = {Atsushi Igarashi and Peter Thiemann and Vasco T. Vasconcelos and Philip Wadler},
journal = {Proceedings of the ACM on Programming Languages},
volume = {1},
number = {ICFP},
year = {2017},
doi = {10.1145/3110282}
}