CAREER: Foundations and Applications of Constraint-based Synthesis
职业:基于约束的综合的基础和应用
基本信息
- 批准号:2049911
- 负责人:
- 金额:$ 52.46万
- 依托单位:
- 依托单位国家:美国
- 项目类别:Continuing Grant
- 财政年份:2021
- 资助国家:美国
- 起止时间:2021-04-01 至 2026-03-31
- 项目状态:未结题
- 来源:
- 关键词:
项目摘要
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 的法定使命,并通过使用基金会的智力价值和更广泛的影响审查标准进行评估,被认为值得支持。
项目成果
期刊论文数量(4)
专著数量(0)
科研奖励数量(0)
会议论文数量(0)
专利数量(0)
Reactamole: Functional Reactive Molecular Programming
Reactamole:功能反应分子编程
- DOI:
- 发表时间:2021
- 期刊:
- 影响因子:0
- 作者:Klinge, Titus H.;Lathrop, James I.;Osera, Peter-Michael;Rogers, Allison
- 通讯作者:Rogers, Allison
Snowflake: Supporting Programming and Proofs
Snowflake:支持编程和证明
- DOI:
- 发表时间:2023
- 期刊:
- 影响因子:0
- 作者: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
- 期刊:
- 影响因子:0
- 作者: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
- 期刊:
- 影响因子:0
- 作者:James I. Lathrop;Peter-Michael Osera;Addison W. Schmidt;Jesse Slater
- 通讯作者:James I. Lathrop;Peter-Michael Osera;Addison W. Schmidt;Jesse Slater
{{
item.title }}
{{ item.translation_title }}
- DOI:
{{ item.doi }} - 发表时间:
{{ item.publish_year }} - 期刊:
- 影响因子:{{ item.factor }}
- 作者:
{{ item.authors }} - 通讯作者:
{{ item.author }}
数据更新时间:{{ journalArticles.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ monograph.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ sciAawards.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ conferencePapers.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ patent.updateTime }}
Peter-Michael Osera其他文献
Constraint-based type-directed program synthesis
- DOI:
10.1145/3331554.3342608 - 发表时间:
2019-07 - 期刊:
- 影响因子:0
- 作者:
Peter-Michael Osera - 通讯作者:
Peter-Michael Osera
Peter-Michael Osera的其他文献
{{
item.title }}
{{ item.translation_title }}
- DOI:
{{ item.doi }} - 发表时间:
{{ item.publish_year }} - 期刊:
- 影响因子:{{ item.factor }}
- 作者:
{{ item.authors }} - 通讯作者:
{{ item.author }}
{{ truncateString('Peter-Michael Osera', 18)}}的其他基金
EAGER: Semi-automated Type-directed Programming
EAGER:半自动类型定向编程
- 批准号:
1651817 - 财政年份:2016
- 资助金额:
$ 52.46万 - 项目类别:
Standard Grant
相似海外基金
CAREER: Solving Estimation Problems of Networked Interacting Dynamical Systems Via Exploiting Low Dimensional Structures: Mathematical Foundations, Algorithms and Applications
职业:通过利用低维结构解决网络交互动力系统的估计问题:数学基础、算法和应用
- 批准号:
2340631 - 财政年份:2024
- 资助金额:
$ 52.46万 - 项目类别:
Continuing Grant
CAREER: On the Foundations of End-to-End Quantum Applications
职业:端到端量子应用的基础
- 批准号:
1942837 - 财政年份:2020
- 资助金额:
$ 52.46万 - 项目类别:
Continuing Grant
CAREER: Algorithmic Foundations and Modern Applications for Program Synthesis
职业:程序综合的算法基础和现代应用
- 批准号:
1652140 - 财政年份:2017
- 资助金额:
$ 52.46万 - 项目类别:
Continuing Grant
CAREER: Human Behavior Assessment from Internet Usage: Foundations, Applications and Algorithms
职业:基于互联网使用的人类行为评估:基础、应用程序和算法
- 批准号:
1559588 - 财政年份:2015
- 资助金额:
$ 52.46万 - 项目类别:
Continuing Grant
CAREER: Anonymous and Robust Multi-Recipient Communication: Foundations and Applications
职业:匿名且稳健的多接收者通信:基础和应用
- 批准号:
1253927 - 财政年份:2013
- 资助金额:
$ 52.46万 - 项目类别:
Continuing Grant
CAREER: Human Behavior Assessment from Internet Usage: Foundations, Applications and Algorithms
职业:基于互联网使用的人类行为评估:基础、应用程序和算法
- 批准号:
1254117 - 财政年份:2013
- 资助金额:
$ 52.46万 - 项目类别:
Continuing Grant
CAREER: Structured Matrix Computations: Foundations, Methods, and Applications
职业:结构化矩阵计算:基础、方法和应用
- 批准号:
1255416 - 财政年份:2013
- 资助金额:
$ 52.46万 - 项目类别:
Continuing Grant
CAREER: Computational Geometric Mechanics: Foundations, Computation, and Applications
职业:计算几何力学:基础、计算和应用
- 批准号:
1010687 - 财政年份:2009
- 资助金额:
$ 52.46万 - 项目类别:
Continuing Grant
CAREER: Computational Geometric Mechanics: Foundations, Computation, and Applications
职业:计算几何力学:基础、计算和应用
- 批准号:
0747659 - 财政年份:2008
- 资助金额:
$ 52.46万 - 项目类别:
Continuing Grant
CAREER: Design, Applications, and Foundations of Safe, Low-Level Programming Languages
职业:安全、低级编程语言的设计、应用和基础
- 批准号:
9875536 - 财政年份:1999
- 资助金额:
$ 52.46万 - 项目类别:
Continuing Grant














{{item.name}}会员




