一句话：提出通用可插拔类型推断算法，复用局部推断，在 Checker Framework 实现，平均减少 45% 待注解警告。
可插拔类型系统用类型限定符（如 nonnull、secret）扩展宿主语言，能发现更多错误，但程序员须手写限定符，这是实际采用的主要障碍。传统类型推断与具体类型系统绑定，每新增系统都要实现约束生成与求解。本文观察到实用可插拔类型系统是流敏感的，已实现局部推断，于是提出迭代式全局推断：每轮复用局部推断为过程和字段生成摘要，后续轮次利用摘要改进全程序推断，直至摘要达到不动点。该算法可在框架层实现一次并被所有类型检查器复用。作者在 Checker Framework 上实现，用 11 个类型系统和 12 个项目评估，平均减少 45% 需通过注解解决的警告。
A pluggable type system extends a host programming language with type qualifiers. It lets programmers write types like unsigned int, secret string, and nonnull object. Typechecking with pluggable types detects and prevents more errors than the host type system. However, programmers must write type qualifiers; this is the biggest obstacle to use of pluggable types in practice. Type inference can solve this problem. Traditional approaches to type inference are type-system-specific: for each new pluggable type system, the type inference algorithm must be extended to build and then solve a system of constraints corresponding to the rules of the underlying type system. We propose a novel type inference algorithm that can infer type qualifiers for any pluggable type system with little to no new type-system-specific code-that is, “for free”. The key insight is that extant practical pluggable type systems are flow-sensitive and therefore already implement local type inference. Using this insight, we can derive a global inference algorithm by re-using existing implementations of local inference. Our algorithm runs iteratively in rounds. Each round uses the results of local type inference to produce summaries (specifications) for procedures and fields. These summaries enable improved inference throughout the program in subsequent rounds. The algorithm terminates when the inferred summaries reach a fixed point. In practice, many pluggable type systems are built on frameworks. By implementing our algorithm once, at the framework level, it can be reused by any typechecker built using that frame-work. Using that insight, we have implemented our algorithm for the open-source Checker Framework project, which is widely used in industry and on which dozens of specialized pluggable typecheckers have been built. In experiments with 11 distinct pluggable type systems and 12 projects, our algorithm reduced, by 45 % on average, the number of warnings that developers must resolve by writing annotations.