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

鉴于软件在现代社会中的核心作用，确保软件可靠运行的工具和技术至关重要。可插拔类型检查已被证明是一种非常有效的技术，可以防止各种各样的软件错误。然而，可插入的类型检查很难采用，因为它需要软件开发人员花费大量时间将额外的注释插入到现有的源代码中。这个项目将开发可插入类型推断的技术，自动插入这些额外的注释。该项目的新颖之处是一套可插入的类型推断算法，它与各种可插入的类型检查器一起工作，推断准确的注释，并扩展到大型软件系统。该项目的影响是显着缓解采用可插拔类型检查现有的代码，从而提高了可靠性和可维护性的真实世界的软件systems.Inference的可插拔类型注释需要高的可扩展性和最大努力的输出程序，不类型检查，属性不提供现有的技术。该项目将开发一套可插拔类型推理方法，适用于处理各种各样的可插拔类型系统和检查器。该项目将探索基于搜索的“黑盒”推理技术，这些技术在类型检查器实现上是通用的;基于框架的“灰盒”推理技术，这些技术可与构建在公共基础设施上的任何类型检查器一起使用;以及专门的“白盒”推理技术，这些技术利用特定于类型系统的推理。此外，该项目将研究新的类型系统和功能，使有效的推理：当类型大多是推断，更复杂和冗长的可插拔类型系统将成为practical.This奖项反映了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.