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

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

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.