Deductive Systems and Optimizing Compilers for Higher-Order Languages

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.