Award Abstract # 2049911
CAREER: Foundations and Applications of Constraint-based Synthesis

NSF Org: CCF
Division of Computing and Communication Foundations
Recipient: THE TRUSTEES OF GRINNELL COLLEGE
Initial Amendment Date: February 24, 2021
Latest Amendment Date: April 9, 2025
Award Number: 2049911
Award Instrument: Continuing Grant
Program Manager: Anindya Banerjee
abanerje@nsf.gov
 (703)292-7885
CCF
 Division of Computing and Communication Foundations
CSE
 Directorate for Computer and Information Science and Engineering
Start Date: April 1, 2021
End Date: March 31, 2026 (Estimated)
Total Intended Award Amount: $524,611.00
Total Awarded Amount to Date: $524,611.00
Funds Obligated to Date: FY 2021 = $224,500.00
FY 2022 = $234,764.00

FY 2025 = $65,347.00
History of Investigator:
  • Peter-Michael Osera (Principal Investigator)
    osera@cs.grinnell.edu
Recipient Sponsored Research Office: Grinnell College
733 BROAD ST
GRINNELL
IA  US  50112-2227
(641)269-4983
Sponsor Congressional District: 02
Primary Place of Performance: Grinnell College
IA  US  50112-1690
Primary Place of Performance
Congressional District:
02
Unique Entity Identifier (UEI): NRFXPGZU88G2
Parent UEI:
NSF Program(s): Software & Hardware Foundation
Primary Program Source: 01002324DB NSF RESEARCH & RELATED ACTIVIT
01002122DB NSF RESEARCH & RELATED ACTIVIT

01002425DB NSF RESEARCH & RELATED ACTIVIT

01002223DB NSF RESEARCH & RELATED ACTIVIT

01002526DB NSF RESEARCH & RELATED ACTIVIT
Program Reference Code(s): 7943, 9150, 1045
Program Element Code(s): 779800
Award Agency Code: 4900
Fund Agency Code: 4900
Assistance Listing Number(s): 47.070

ABSTRACT

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.

PUBLICATIONS PRODUCED AS A RESULT OF THIS RESEARCH

Note:  When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external site maintained by the publisher. Some full text articles may not yet be available without a charge during the embargo (administrative interval).

Some links on this page may take you to non-federal websites. Their policies may differ from this site.

Alabi, Oluwatobi and Vu, Anh and Osera, Peter-Michael "Snowflake: Supporting Programming and Proofs" SIGCSE 2023: Proceedings of the 54th ACM Technical Symposium on Computer Science Education , v.2 , 2023 Citation Details
Klinge, Titus H and Lathrop, James I and Osera, Peter-Michael and Rogers, Allison "Reactamole: functional reactive molecular programming" Natural Computing , 2024 https://doi.org/10.1007/s11047-024-09982-5 Citation Details
Klinge, Titus H. and Lathrop, James I. and Osera, Peter-Michael and Rogers, Allison "Reactamole: Functional Reactive Molecular Programming" 27th International Conference on DNA Computing and Molecular Programming (DNA 27) , v.205 , 2021 Citation Details
Lathrop, James I. and Osera, Peter-Michael and Schmidt, Addison W. and Slater, Jesse C. "Verifying Chemical Reaction Networks with the Isabelle Theorem Prover" 2023 59th Annual Allerton Conference on Communication, Control, and Computing (Allerton) , 2023 https://doi.org/10.1109/Allerton58177.2023.10313474 Citation Details
Worden, Eamon and Song, Olivia and Osera, Peter-Michael "Notional Machine in Mathematics and Introductory Computer Science Courses" SIGCSE 2023: Proceedings of the 54th ACM Technical Symposium on Computer Science Education , v.2 , 2022 https://doi.org/10.1145/3545947.3576324 Citation Details

Please report errors in award information by writing to: awardsearch@nsf.gov.

Print this page

Back to Top of page