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

PI: Kfoury, Assaf j .提案编号：9988529机构：Boston university提议的研究，从广义上讲，是在类型论和重写理论，单独或结合，由编程语言的设计和实现问题的动机。特别感兴趣的主题包括：自动类型推断、语言特性的表达性、实现的效率、可靠性以及对上述所有内容之间权衡的分析。在两位主要研究者和他们的合作者过去在类型化lambda演算、函数式语言和重写系统方面的研究的基础上，拟议的研究将扩展到更丰富的类型化lambda演算，主要基于交集和联合类型，以支持更好的设计和实现高阶类型语言。这与过去在处理相同问题时使用普遍类型和存在类型不同。提出的转变是合理的，因为使用通用类型导致了一些复杂的情况，自20世纪90年代初以来，由两位主要研究者和许多其他研究人员发现；相比之下，最近的研究表明，在基于交集类型的类型化lambda演算中不会遇到这些并发症。所提出的研究的最终目标是为使用显式类型中间语言实现类型导向和流导向编译器提供严格和正式的基础。这样的编译器将遵守一个不变量，即在编译过程的每个阶段，程序的中间表示都将是良好的类型。目前正在开发一种类型化的中间语言，它基于一种既便于流导向优化又便于类型导向优化的设计。

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.