CRII: SHF: Bespoke Data Representation Synthesis via Contextual Data Refinement

CRII：SHF：通过上下文数据细化定制数据表示合成

基本信息

批准号：
1755880
负责人：
Benjamin Delaware
金额：
$ 16.32万
依托单位：
Purdue University
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2018
资助国家：
美国
起止时间：
2018-08-15 至 2021-07-31
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=1755880&HistoricalAwards=false
关键词：
CRII SHF Bespoke Data Representation

项目摘要

Nearly every modern programming language provides some mechanism for hiding the implementation details of reusable components behind some abstract interface. This interface acts as a contract, enforced by the language, that benefits both the developers and clients of such components: protecting the developers? design decisions from clients and enabling clients to safely swap in different implementations of the same interface. Recent advances in program synthesis have shown how custom implementations can be automatically built from high-level specifications of a client?s requirements, exploiting this contract to ensure that synthesized components satisfy the desired requirements. Existing approaches to language-enforced abstraction approaches can be too restrictive in this setting, however, as they require the synthesized implementation to work for any client. This disallows any implementations whose correctness are dependent on a particular client?s usage. The goal of this project is to relax this condition, enabling the synthesis of custom implementations that are tailored to a particular client while still providing the same strong abstraction guarantees that programmers expect from their programming languages. The intellectual merits are the development of a refined notion of modularity in programming languages, advancing the state of the art in the synthesis of correct, performant code. The project's broader significance and importance are the development of an approach that allows programmers to program against high-level abstractions without paying a performance penalty.The project advances the state of the art in both the theoretical foundations of data abstraction and the development of verified software. The vehicle for the work's theoretical contributions is a formalization of a core calculus for data refinement. This calculus is used to reformulate the well-established notion of data refinement for abstract data types (ADTs) to incorporate information about a specific client's usage of an interface. A key component is the development of the metatheory proofs establishing that the standard property of representation independence under data refinement is preserved. This approach is used to improve the existing Fiat deductive synthesis framework, enabling clients to derive verified ADT implementations that are tailored to their particular usage. The augmented system is evaluated via the synthesis of custom implementations of the popular Haskell bytestring library for two open-source Haskell programs, using an existing derivation of a performant bytestring implementation in Fiat as a starting point.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

几乎每种现代编程语言都提供了一些机制，可以将可重复使用组件的实现细节隐藏在某些抽象界面之后。该界面充当由语言执行的合同，使这些组件的开发人员和客户都受益：保护开发人员？设计客户的决策，并使客户能够在同一界面的不同实现中安全地交换。程序合成的最新进展表明，如何自动实现如何从客户要求的高级规格中构建，并利用本合同以确保合成的组件满足所需的要求。但是，在这种情况下，现有的语言提出抽象方法的方法可能过于限制，因为它们要求合成的实施能够为任何客户使用。这将取消任何正确性取决于特定客户端的使用的实现。该项目的目的是放松这种情况，使能够为特定客户量身定制的自定义实现综合，同时仍然提供相同的强大抽象保证了程序员从其编程语言中期望的。智力优点是在编程语言中的模块化概念的发展，在综合正确的，性能的代码的综合中推进了最新的状态。该项目的更广泛的意义和重要性是开发一种方法，该方法使程序员能够在不支付绩效罚款的情况下针对高级抽象进行编程。该项目在数据抽象的理论基础和经过验证的软件的开发中都可以提高最新技术的状态。该工作理论贡献的工具是对数据改进的核心演算的形式化。该演算用于重新制定摘要数据类型（ADT）的数据完善概念，以结合有关特定客户端对接口的使用的信息。一个关键的组成部分是开发元理性证明，以表明在数据完善下保留了表示独立性的标准特性。这种方法用于改善现有的菲亚特演绎合成框架，使客户能够得出根据其特定用法量身定制的经过验证的ADT实现。通过合成两个开源的Haskell程序的自定义实现，使用了FIAIT中表现的BYTESTRING实现的现有推导作为起点，该奖项反映了NSF的法定任务，并通过评估基金会的智力综述，该奖项反映了NSF的法定任务，该奖项是通过合成流行的Haskell Bytestring库的自定义实现来评估的。