一句话：为 π-演算提出两个类型系统，可从类型推导提取并行计算中 work 与 span 的复杂度界。
函数式语言的类型系统已被广泛用于分析和控制程序，并能从类型推导中提取复杂度界，但这类结果尚未很好扩展到并行计算。本文在 π-演算这一基于通信的并行计算模型中研究并行复杂度，区分两种时间复杂度：无并行时的总计算时间 work，以及最大并行下的计算时间 span。作者定义操作语义以刻画这两个概念，并提出两个类型系统，分别受 sized types 与 input/output types 启发，并加入关于通信的时间信息。其目标是使类型推导能够给出进程的复杂度界，从而把静态复杂度分析技术从函数式语言推广到通信式并行进程演算。
Type systems as a technique to analyse or control programs have been extensively studied for functional programming languages. In particular, some systems allow one to extract from a typing derivation a complexity bound on the program. We explore how to extend such results to parallel complexity in the setting of pi-calculus, considered as a communication-based model for parallel computation. Two notions of time complexity are given: the total computation time without parallelism (the work) and the computation time under maximal parallelism (the span). We define operational semantics to capture those two notions and present two type systems from which one can extract a complexity bound on a process. The type systems are inspired both by sized types and by input/output types, with additional temporal information about communications.
@article{paperbot1613,
title = {Types for Complexity of Parallel Computation in Pi-calculus},
author = {Patrick Baillot and Alexis Ghyselen},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {44},
number = {3},
year = {2022},
doi = {10.1145/3495529}
}