Implementing Modular Program Analysis via Intersection and Union Types.
PI: Assaf J. Kfoury
The proposed research will investigate real-world relevance of a new framework for modular program-analysis, which uses "intersection" and "union" types. The starting point of this investigation is a recently designed polymorphic type system, called System I, for a foundational functional language, the lambda-calculus. The chief feature of System I is the use of "intersection" types together with the new technology of "expansion variables", which allow System I to satisfy a substitution-based principal-typings property. Although fully modular, the resulting program analysis is now restricted to a foundational language (the lambda-calculus) missing many standard high-level programming features such as conditionals, recursive definitions, exceptions, assignments, input/output, etc. Considerable work is necessary in order to turn System I into a type system for a full-fledged programming language such as Scheme (now considered to be the initial target language of proposed research).
The proposed research is largely engineering work, aimed at producing an efficient prototype implementation, based on appropriate extensions of System I. The implementation will be evaluated --- or re-designed in parts --- by the extent to which it produces demonstrably better results in handling large software systems (enforcing larger classes of safety properties, statically detecting and ruling out larger classes of run-time errors).
