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.