ITR/SY (CCR): Implementing Modular Program Analysis via Intersection and Union Types

ITR/SY (CCR)：通过交集和并集类型实施模块化程序分析

• 批准号: 0113193
• 负责人: Assaf Kfoury
• 金额: $ 44.84万
• 依托单位: Trustees of Boston University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2001
• 资助国家: 美国
• 起止时间: 2001-09-01 至 2005-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0113193&HistoricalAwards=false
• 关键词: ITR; SY; CCR; Implementing; Modular

Proposal Number: ITR Proposal 0113193Title: Implementing Modular Program Analysis via Intersectionand Union Types.PI: Assaf J. KfouryThe 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).

提案号：ITR提案0113193标题：通过交集和联合类型实现模块化程序分析。PI: Assaf J. kfoury提议的研究将调查模块化程序分析的新框架在现实世界中的相关性，该框架使用“交集”和“联合”类型。这项研究的起点是最近设计的一个多态类型系统，称为系统I，用于基本的函数式语言，lambda-calculus。系统I的主要特点是使用了“交集”类型和“展开变量”的新技术，这使得系统I能够满足基于替换的主类型属性。虽然完全模块化，结果程序分析现在仅限于基础语言（lambda演算），缺少许多标准的高级编程功能，如条件，递归定义，异常，赋值，输入/输出等。为了将System I转变为成熟的编程语言（如Scheme）的类型系统（现在被认为是建议研究的初始目标语言），需要进行大量的工作。拟议的研究主要是工程工作，旨在基于系统i的适当扩展产生有效的原型实现。实现将被评估——或部分重新设计——根据它在处理大型软件系统时产生明显更好的结果的程度（强制更大类别的安全属性，静态检测和排除更大类别的运行时错误）。