A Paradigm Shift in Program Analysis and Transformation via Intersection and Union Types

点击翻译按钮获取中文摘要

PI: Kfoury, Assaf J.Proposal Number: 9988529Institution: Boston UniversityThe proposed research is, broadly speaking, in type theory and rewriting theory, separately and in com-bination, motivated by issues of design and implementation of programming languages. Topics of special interest include: automated type inference, expressiveness of language features, efficiency of implementations, reliability, and analysis of tradeoffs between all of the preceding.Building on past research by the 2 principal investigators and their collaborators in typed lambda calculi, functional languages and rewriting systems, the proposed research will extend to richer typed lambda calculi, mostly based on intersection and union types, towards supporting better design and implementation of higher-order typed languages. This is a shift from the use of universal and existential types in addressing the same issues in the past. The proposed shift is justified by several complications resulting from the use of universal types, discovered by the 2 principal investigators and many other researchers since the early 1990's; by contrast, very recent research shows that these complications are not encountered in typed lambda calculi based on intersection types.The ultimate goal of the proposed research is to provide a rigorous and formal foundation for the imple-mentation of a type-directed and flow-directed compiler using an explicitly typed intermediate language. Such a compiler will observe the invariant that at each stage of the compilation process the intermediate representation of the program will be well typed. A typed intermediate language is currently developed, based on a design to facilitate both flow-directed and type-directed optimization.