Deductive Systems and Optimizing Compilers for Higher-Order Languages

9900918 Hannan，John J.本研究研究基于类型的演绎系统和优化高阶语言编译器的算法的形式规范，分析和实现。 类型理论和演绎系统是用于设计和规范编程语言的重要工具，但这些工具尚未广泛用于优化语言编译器的设计和实现。 相反，控制流分析为高阶语言的编译器中的许多优化提供了主要基础。 本研究旨在推进基于类型和演绎系统的编译器优化的状态，补充控制流分析的工作。 具体活动包括：（1）开发新的、基于类型的演绎系统，指定新的和现有的编译器优化/翻译;（2）开发演绎系统的一般理论和用于编译器优化的相关算法，以及基于该理论的原型实现;以及（3）基于使用这些结果构造优化编译器的实验实现。 总之，这些目标有助于通过研究基于类型的优化在这些语言上的理论和实际应用来推进高阶语言实现的状态，补充现有技术。

9900918 Hannan, John J.This research studies the formal specification, analysis, and implementation of type-based deductive systems and algorithms for optimizing compilers of higher-order languages. Type theory and deductive systems are important tools used in the design and specification of programming languages, but these tools have not been extensively used in the design and implementation of optimizing compilers for languages. Instead, control-flow analyses have provided the primary basis for many optimizations in compiler for higher-order languages. This research seeks to advance the state of compiler optimizations based on types and deductive systems, complementing the work on control-flow analyses. Specific activities include: (1) developing new, type-based deductive systems specifying new and existing compiler optimizations/translations; (2) developing a general theory of deductive systems and related algorithms for compiler optimizations, and a prototype implementation based on this theory; and (3) constructing an experimental implementation of an optimizing compiler based on using these results. Together, these objectives serve to advance the state of higher-order language implementations by studying the theoretical and practical application of type-based optimizations on these languages, complementing existing technologies.