一句话：提出基于非幂等交集类型的 π 演算类型系统，刻画无运行时错误且可“完成工作”的进程，并证明其完备性。
本文为 π 演算引入一个类型系统，目标是用类型保证进程行为良好：可类型化进程永不产生运行时错误，并且即使可能发散，也总有机会归约到空闲进程，即“完成工作”。该系统基于非幂等交集类型，因此能捕获的进程类非常广。尽管所刻画的底层行为性质是 Π2^0-完全的，作者仍证明该系统是完备的：任何行为良好的进程都可被类型化，只是显然需要考虑无穷多个推导。
We introduce a type system for the π-calculus which is designed to guarantee that typable processes are well-behaved , namely they never produce a run-time error and, even if they may diverge, there is always a chance for them to “finish their work”, i.e., to reduce to an idle process. The introduced type system is based on non-idempotent intersections, and is thus very powerful as for the class of processes it can capture. Indeed, despite the fact that the underlying property is Π 2 0 -complete, there is a way to show that the system is complete , i.e., that any well-behaved process is typable, although for obvious reasons infinitely many derivations need to be considered.
@article{paperbot644,
title = {Intersection types and runtime errors in the pi-calculus},
author = {Ugo Dal Lago and Marc de Visme and Damiano Mazza and Akira Yoshimizu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290320}
}