Types for 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. ***