Collaborative Research: SHF: MEDIUM: General and Scalable Pluggable Type Inference

鉴于软件在现代社会中的核心作用，确保该软件可靠运行的工具和技术至关重要。可插拔类型检查已被证明是防止各种软件错误的一种非常有效的技术。然而，可插拔类型检查很难采用，因为它需要软件开发人员花费大量时间在其现有源代码中插入额外的注释。该项目将开发可插拔类型推断的技术，自动插入这些额外的注释。该项目的新奇之处在于一套可插拔的类型推断算法，这些算法可与各种可插拔的类型检查器一起工作，推断准确的注释，并扩展到大型软件系统。该项目的影响是大大简化了对现有代码采用可插拔类型检查，从而提高了真实软件系统的可靠性和可维护性。可插拔类型注释的引用需要对不进行类型检查的程序具有高可伸缩性和尽力而为输出，这是现有技术所不提供的特性。该项目将开发一套可插拔类型推理方法，适用于处理各种可插拔类型系统和检查器。该项目将探索基于搜索的“黑盒”推理技术，它是类型检查器实现上的通用技术；基于框架的“灰盒”推理技术，它与建立在公共基础设施上的任何类型检查器一起工作；以及专门的“白盒”推理技术，它利用特定于类型系统的推理。此外，该项目将调查由有效推理实现的新类型系统和功能：当类型主要被推断时，更复杂和冗长的可插拔类型系统将变得实用。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Given the central role of software in modern society, tools and techniques that ensure this software behaves reliably is of critical importance. Pluggable type checking has been shown to be a highly effective technique for preventing a wide variety of software bugs. However, pluggable type checking is difficult to adopt, as it requires software developers to spend significant time inserting additional annotations into their existing source code. This project will develop techniques for pluggable type inference, automating the insertion of these additional annotations. The project's novelties are a suite of pluggable type inference algorithms that work with a wide variety of pluggable type checkers, infer accurate annotations, and scale to large software systems. The project's impacts are significantly easing the adoption of pluggable type checking for existing code, thereby improving the reliability and maintainability of real-world software systems.Inference of pluggable type annotations requires high scalability and best-effort output for programs that do not type check, properties not provided by existing techniques. The project will develop a suite of pluggable type inference approaches, suitable for handling a wide variety of pluggable type systems and checkers. The project will explore search-based, "black-box" inference techniques that are generic over the type checker implementation; framework-based, "gray-box" inference techniques that work with any type checker built on common infrastructure; and specialized "white-box" inference techniques that utilize type-system-specific reasoning. Additionally, the project will investigate new type systems and features enabled by effective inference: when types are mostly inferred, more complex and verbose pluggable type systems will become practical.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.