CAREER: Foundations and Applications of Constraint-based Synthesis

职业：基于约束的综合的基础和应用

• 批准号: 2049911
• 负责人: Peter-Michael Osera
• 金额: $ 52.46万
• 依托单位: Grinnell College
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2021
• 资助国家: 美国
• 起止时间: 2021-04-01 至 2026-03-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2049911&HistoricalAwards=false
• 关键词: CAREER; Foundations; Applications; Constraint; based

Program synthesis promises to democratize programming for the masses by automating the generation of tedious, error-prone code from more natural and understandable user-provided specification. Over the past two decades, advances in computational power have led to a proliferation of program-synthesis techniques that draw upon various fields ranging from logic, programming-language theory, and machine learning. These techniques differ substantially in how they operate, and no single technique is universally superior in all cases. Furthermore, little is understood about users' actual needs and sentiment towards advanced development tools like synthesizers, which inevitably leads to the development of theoretically interesting but ultimately uncompelling or impractical tools. The novelties of this project are two-fold: (a) providing a unifying framework for these differing techniques so that their theoretical underpinnings can be better understood and next-generation program synthesis tools can be built on top of this framework, and (b) identifying the set of human factors that should be considered when making program-synthesis tools. This project's impact is, ultimately, unifying perspectives on program synthesis not just in terms of techniques but also disciplines: programming languages, human-computing interaction, and computer-science education.The project focuses on two primary efforts. The first is developing a unified set of semantic foundations for synthesis based on a generalized notion of constraint that captures the common forms of specifications found with current techniques, e.g., types, examples, logical constraints, syntactic constraints, and partial programs. This constraint-based approach to synthesis naturally leads to a deductive, hole-guided programming style, different from traditional programming models. Therefore, the project's second effort is a systematic study of the needs and sentiment of developers towards this style of programming and the design of next-generation development tools based on these results.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.

计划合成有望通过从更自然和可以理解的用户提供的规范中自动化繁琐的，容易出错的代码来使群众民主化。在过去的二十年中，计算能力的进步导致了程序合成技术的扩散，这些技术借鉴了逻辑，编程语言理论和机器学习的各种领域。这些技术在其运作方式上有很大差异，并且在所有情况下，任何单一技术都没有普遍优势。此外，对用户对诸如合成器等先进开发工具的实际需求和情感几乎没有理解，这不可避免地会导致理论上有趣但最终不兼容或不切实际的工具的开发。该项目的新颖性是两个方面的：（a）为这些不同的技术提供一个统一的框架，以便可以更好地理解其理论基础，并可以在此框架的顶部构建下一代程序综合工具，以及（b）确定制造程序合理工具时应考虑的人为因素的集合。最终，该项目的影响是统一对计划综合的观点，不仅是在技术方面，而且还统一了学科：编程语言，人为计算的互动和计算机科学教育。该项目侧重于两项主要努力。第一个是基于概述的广义概念开发统一的综合语义基础，该概念捕获了使用当前技术（例如类型，示例，逻辑约束，句法约束和部分程序）发现的常见规格形式。这种基于约束的综合方法自然会导致一种演绎的，洞引导的编程样式，与传统编程模型不同。因此，该项目的第二次努力是对开发人员对这种编程方式的需求和情感的系统研究，并基于这些结果设计了下一代开发工具的设计。该奖项反映了NSF的法定任务，并被认为是值得通过基金会的知识分子优点和更广泛影响的评估来评估的。

项目成果

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

Snowflake: Supporting Programming and Proofs

Snowflake：支持编程和证明

• 发表时间: 2023
• 期刊: SIGCSE 2023: Proceedings of the 54th ACM Technical Symposium on Computer Science Education
• 作者: Alabi, Oluwatobi;Vu, Anh;Osera, Peter-Michael
• 通讯作者: Osera, Peter-Michael

Notional Machine in Mathematics and Introductory Computer Science Courses

数学和计算机科学入门课程中的概念机

• DOI: 10.1145/3545947.3576324
• 发表时间: 2022
• 期刊: SIGCSE 2023: Proceedings of the 54th ACM Technical Symposium on Computer Science Education
• 作者: Worden, Eamon;Song, Olivia;Osera, Peter-Michael
• 通讯作者: Osera, Peter-Michael

Verifying Chemical Reaction Networks with the Isabelle Theorem Prover

• DOI: 10.1109/allerton58177.2023.10313474
• 发表时间: 2023-09
• 期刊: 2023 59th Annual Allerton Conference on Communication, Control, and Computing (Allerton)
• 作者: James I. Lathrop;Peter-Michael Osera;Addison W. Schmidt;Jesse Slater