Analysis-Based Program Transformation

CCR-9804115这个项目试图理解程序分析如何证明通常基于它的程序转换是合理的。许多有趣的优化依赖于过程间分析，它收集关于大于单个过程的程序单元的信息。这种优化在高阶语言中很普遍，如Scheme或ML，并且在普通的命令式语言中也起着重要作用。尽管在抽象解释和相关的分析框架上已经有几十年的工作，但仍然很少有分析实际用于证明相关转换的正确性的例子。这个项目试图通过做一系列与高阶“几乎函数式”语言（如Scheme或ML）的编译相关的示例来填补这一空白。 它还试图将基于分析的转换与基于上下文等价的转换理论统一起来，并将所有这些理论扩展到包含并行或分布式计算的程序。

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