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

RUI：可证明安全性，可提高性能的基于自由定理的程序转换

基本信息

批准号：
0429072
负责人：
Patricia Johann
金额：
$ 12.38万
依托单位：
Rutgers University New Brunswick
依托单位国家：
美国
项目类别：
Continuing Grant
财政年份：
2004
资助国家：
美国
起止时间：
2004-08-15 至 2008-07-31
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=0429072&HistoricalAwards=false
关键词：
RUI Provable Safety Performance Improving

项目摘要

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.

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