Analysis-Based Program Transformation

点击翻译按钮获取中文摘要

CCR-9804115 This project seeks to understand how a program analysis justifies the program transformation that is typically based upon it. Many interesting optimizations depend on interprocedural analyses, which collect information about program units larger than a single procedure. Such optimizations are widespread in higher- order languages such as Scheme or ML, and play an important role in ordinary imperative languages as well. Despite decades of work on abstract interpretation and related analysis frameworks, there are still very few examples in which an analysis is actually used to prove the correctness of an associated transformation. This project seeks to fill this gap by doing a series of examples related to the compilation of higher-order ``almost-functional'' languages like Scheme or ML. It also seeks to unify analysis-based transformations with the theory of transformations based on contextual equivalence, and to extend all of this theory to embrace programs that compute in parallel or distributed settings.***