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

合作研究：SHF：MEDIUM：通用且可扩展的可插入类型推理

• 批准号: 2312262
• 负责人: Martin Kellogg
• 金额: $ 45万
• 依托单位: New Jersey Institute of Technology
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-07-01 至 2027-06-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2312262&HistoricalAwards=false
• 关键词: Collaborative; Research; SHF; MEDIUM; General

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.

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