一句话：提出时间会话类型，将线性逻辑会话类型扩展以局部、组合地分析并发消息传递程序的参数化并行复杂度。
本文研究并发消息传递程序的参数化并行复杂度分析。为使分析局部且可组合，作者对二元会话类型进行保守扩展，并利用其与直觉主义线性逻辑的 Curry–Howard 对应。核心创新是引入时间模态 next、always、eventually，从而在类型中精确而灵活地规定消息交换的时序。所得时间会话类型可统一表达消息速率、流水线延迟、并发队列响应时间以及 fork/join 并行程序的 span 等性质。该分析对成本模型参数化，并以通信成本为例进行展示。作者使用带时间的多重集重写语义证明 progress 与类型保持，从而建立分析的可靠性。代表性例子说明了该方法的适用范围与可用性。
We study the problem of parametric parallel complexity analysis of concurrent, message-passing programs. To make the analysis local and compositional, it is based on a conservative extension of binary session types, which structure the type and direction of communication between processes and stand in a Curry-Howard correspondence with intuitionistic linear logic. The main innovation is to enrich session types with the temporal modalities next (◯ A ), always (□ A ), and eventually (◇ A ), to additionally prescribe the timing of the exchanged messages in a way that is precise yet flexible. The resulting temporal session types uniformly express properties such as the message rate of a stream, the latency of a pipeline, the response time of a concurrent queue, or the span of a fork/join parallel program. The analysis is parametric in the cost model and the presentation focuses on communication cost as a concrete example. The soundness of the analysis is established by proofs of progress and type preservation using a timed multiset rewriting semantics. Representative examples illustrate the scope and usability of the approach.
@article{paperbot275,
title = {Parallel complexity analysis with temporal session types},
author = {Ankush Das and Jan Hoffmann and Frank Pfenning},
journal = {Proceedings of the ACM on Programming Languages},
volume = {2},
number = {ICFP},
year = {2018},
doi = {10.1145/3236786}
}