Types for Software Systems

软件系统的类型

• 批准号: 9619843
• 负责人: Scott Smith
• 金额: $ 20.72万
• 依托单位: Johns Hopkins University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1997
• 资助国家: 美国
• 起止时间: 1997-07-01 至 2000-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9619843&HistoricalAwards=false
• 关键词: Types; Software; Systems

9619843 This research project lies in the area of developing expressive type systems for programming languages. Expressive type disciplines enable more programs to typecheck, and thus support more diverse styles of programming. Constrained types are a new type form that is particularly rich, but many research challenges must be solved before they will be practical. Constrained types are studied with the aim to increase type expressiveness, as well as to apply constrained types to program analysis: these types have recently been shown to be isomorphic to well-known flow analysis algorithms performed by compilers. The project will explore this flow-types duality to (1) Systematize and add rigor to flow algorithm descriptions; (2) Improve the precision of type systems; (3) Develop and implement improved type inference algorithms; (4) Improve the quality of flow analysis algorithms; and (5) Improve the usefulness of typed intermediate languages in compilation. Successful completion of the research will contribute to the quality of (1) Programming languages, by developing richer type systems; (2) Compilers, by enhancing the quality of optimizations possible via better program analyses; (3) CASE tools, by developing both richer algorithms for type inference and a rich suite of flow-based tools to elucidate program function. ***

9619843这个研究项目属于为编程语言开发表达型系统的领域。表达型原则使更多的程序能够进行类型检查，从而支持更多样化的编程风格。约束类型是一种特别丰富的新型类型形式，但在实际应用之前必须解决许多研究挑战。研究约束类型的目的是增加类型表达性，以及将约束类型应用于程序分析：这些类型最近被证明与编译器执行的众所周知的流分析算法是同构的。该项目将探索这种流类型的二元性，以(1)系统化并增加流算法描述的严谨性；(2)提高类型系统的精度；(3)开发和实现改进的类型推断算法；(4)提高流量分析算法的质量；(5)提高类型化中间语言在编译中的实用性。研究的成功完成将有助于提高(1)编程语言的质量，通过开发更丰富的类型系统；(2)编译器，通过更好的程序分析来提高优化的质量；(3) CASE工具，通过开发更丰富的类型推断算法和一套丰富的基于流的工具来阐明程序功能。＊＊＊