RUI: Provable Safety for Performance-Improving Free Theorems-Based Program Transformations

建议编号0429072基于自由定理的程序转换的可证明安全性帕特里夏·约翰·罗格斯大学，新不伦瑞克这项研究的重点是形式化证明某些转换的安全性的技术，这些转换提高了用纯函数式语言编写的程序的性能。所考虑的变换是基于所谓的“不等式自由定理”。这种转换通过自动从统一处理数据的程序中移除数据构造函数和其他数据操作操作符，可以显著降低函数式语言中的可表现性和效率之间的紧张关系；正式的安全性证明确保这样做的转换不会以意想不到的方式改变它们所应用到的程序的可观察行为。考虑了纯严格函数式语言、带有显式惰性注释的严格函数式语言和具有多态严格原语的非严格语言的基于不等式自由定理的程序转换，并研究了它们的可证明安全性的可操作的、外指的、基于语义的方法。此外，还使用限定类型系统对非严格的函数式语言的标准方程自由定理的弱化方式进行了细粒度的分析。

Proposal Number 0429072Provable Safety for Performance-Improving Free Theorems-Based Program TransformationsPatricia JohannRutgers University New BrunswickThis research focuses on techniques for formally proving the safety of certain transformations which improve the performance of programs written in pure functional languages. The transformations under consideration are based on so-called "inequational free theorems". Such transformations can significantly reduce the tension between expressivity and efficiency in functional languages by automatically removing data constructors and other data-manipulating operators from programs which process data uniformly; formal proofs of safety ensure that transformations which do so do not alter in unexpected ways the observable behavior of the programs to which they are applied. Inequational free theorems-based program transformations for purely strict functional languages, strict functional languages with explicit laziness annotations, and nonstrict languages with polymorphic strictness primitives are considered, and operational, as well as denotational, semantics-based approaches to their provable safety are investigated. In addition, qualified type systems are used to conduct a fine-grained analysis of the ways in which the standard equational free theorems for nonstrict languages are weakened for functional languages which are not purely nonstrict.