EAGER: Semi-automated Type-directed Programming

EAGER：半自动类型定向编程

• 批准号: 1651817
• 负责人: Peter-Michael Osera
• 金额: $ 16万
• 依托单位: Grinnell College
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2016
• 资助国家: 美国
• 起止时间: 2016-09-01 至 2019-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1651817&HistoricalAwards=false
• 关键词: EAGER; Semi; automated; Type; directed

Type-directed programming is a powerful programming paradigm found in strongly-typed functional languages where the types of a program are used to guide its development. Users of such languages frequently comment that their programs "write themselves" once they declare the appropriate types. In reality, the actual development process is far from automatic; developers still must apply manual reasoning principles to derive their program even though many of their choices are forced by the language's type system. This project aims to mechanize the type-directed programming process by leveraging techniques from program synthesis and type theory. The intellectual merits of this project are twofold: (1) the expansion of the theoretical foundations of program synthesis with types and (2) the application of these foundations towards program assistance tools that aid in type-directed programming. Beyond merely providing a tool that enhances the productivity of current functional programmers, the project's broader significance and importance is the crystallization of the benefits of type-directed programming in a form that allow non-functional programmers to understand, appreciate, and directly benefit from this programming paradigm.The project extends prior work in the foundations of program synthesis with types, addressing issues of expressiveness and scalability encountered when adopting these foundations into synthesis tools. Notably, the project unifies type-based and verification-based approaches to program synthesis, allowing rich support for both algebraic and primitive data types as well as providing a common framework for understanding both styles of synthesis. In addition, the project investigates semi-automated, rather than fully-automated, program synthesis where the user interacts with the synthesis tool throughout the synthesis process. The basis of this approach lies in adopting the refinement tree, a data structure that captures the potential shapes of programs that a synthesizer can produce, into a useful data structure for visualizing and interacting with this tool. By pursuing semi-automated synthesis, these tools scale up to real-world programming environments by using the developer as an oracle whenever the tool would otherwise take too long or get stuck searching for a solution.

类型导向编程是强类型函数式语言中的一种强大的编程范式，其中程序的类型用于指导其开发。这类语言的用户经常评论说，一旦他们声明了适当的类型，他们的程序就“自己写”了。实际上，实际的开发过程远非自动化;开发人员仍然必须应用手动推理原则来派生他们的程序，即使他们的许多选择是由语言的类型系统强制的。这个项目的目的是机械化的类型导向的编程过程中，利用技术从程序合成和类型理论。这个项目的智力价值是双重的：（1）扩展了程序类型综合的理论基础，（2）将这些基础应用于程序辅助工具，以帮助类型导向编程。除了仅仅提供一个工具来提高当前函数式程序员的生产力之外，该项目更广泛的意义和重要性是以一种允许非函数式程序员理解、欣赏并直接受益于这种编程范式的形式结晶了类型导向编程的好处。该项目扩展了先前在类型程序合成基础上的工作，解决将这些基础应用到合成工具中时遇到的表现力和可扩展性问题。值得注意的是，该项目统一了基于类型和基于验证的方法来进行程序合成，允许对代数和原始数据类型的丰富支持，并为理解这两种风格的合成提供了一个通用框架。 此外，该项目调查半自动化，而不是全自动化，程序合成，用户在整个合成过程中与合成工具进行交互。这种方法的基础在于采用细化树，一种捕获合成器可以产生的程序的潜在形状的数据结构，将其转化为用于可视化和与该工具交互的有用数据结构。通过追求半自动化的合成，这些工具可以扩展到现实世界的编程环境，只要工具需要太长时间或陷入寻找解决方案的困境，就可以将开发人员用作Oracle。

项目成果

Reactamole: Functional Reactive Molecular Programming

Reactamole：功能反应分子编程

• 发表时间: 2021
• 期刊: 27th International Conference on DNA Computing and Molecular Programming (DNA 27
• 作者: Klinge, Titus H.;Lathrop, James I.;Osera, Peter-Michael;Rogers, Allison
• 通讯作者: Rogers, Allison

Constraint-based type-directed program synthesis

• DOI: 10.1145/3331554.3342608
• 发表时间: 2019-07
• 期刊: Proceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven Development
• 作者: Peter-Michael Osera