Program Synthesis with Lightweight Abstractions
Sankha Guria
Friday, May 5, 2023, 10:00 am-12:00 pm 
Abstract
The world is increasingly reliant on software systems of unprecedented scale, while our methods for developing software still require programmers to manually write code with little help in ensuring software correctly meets its intent. Program synthesis, which automatically generates correct programs from specifications, offers a hopeful path forward. While program synthesis has had many successes in recent years, these have mostly been in restricted domains; synthesis has not yet proved useful for the practicing software engineer.
This dissertation advances the science of program synthesis to meet the challenges posed by the use of modern general-purpose languages, tools, and frameworks. In this talk, I will present a work towards an automated programming stack that uses specifications and expressive test cases written by programmers to scale synthesis tools to diverse domains. Specifically, I show that types enriched with effect descriptors inferred from test cases are a potent means to guide the synthesis of real Ruby on Rails web apps or types enriched with logical predicates can be used to synthesize verified privacy preserving queries. The key to both projects, and most other successful synthesis work, is the proper choice of abstraction for the problem domain at hand. Based on this insight, I will describe a new synthesis framework that captures many different synthesis approaches from the literature, making it easier to build the synthesis tools of the future. Finally, I will present a vision for an automated programming stack that uses specifications and expressive test cases written by programmers to scale synthesis tools to diverse domains, moving us closer to a world in which correct programs are constructed automatically from a programmer's intent.
This dissertation advances the science of program synthesis to meet the challenges posed by the use of modern general-purpose languages, tools, and frameworks. In this talk, I will present a work towards an automated programming stack that uses specifications and expressive test cases written by programmers to scale synthesis tools to diverse domains. Specifically, I show that types enriched with effect descriptors inferred from test cases are a potent means to guide the synthesis of real Ruby on Rails web apps or types enriched with logical predicates can be used to synthesize verified privacy preserving queries. The key to both projects, and most other successful synthesis work, is the proper choice of abstraction for the problem domain at hand. Based on this insight, I will describe a new synthesis framework that captures many different synthesis approaches from the literature, making it easier to build the synthesis tools of the future. Finally, I will present a vision for an automated programming stack that uses specifications and expressive test cases written by programmers to scale synthesis tools to diverse domains, moving us closer to a world in which correct programs are constructed automatically from a programmer's intent.
Examining Committee
Bio
Sankha Narayan Guria is a PhD student at the Department of Computer Science at the University of Maryland, College Park, advised by Prof. David Van Horn and Prof. Jeff Foster. He is a member of the Programming Languages at University of Maryland (PLUM) group. His research focuses on the design, and implementation of program synthesis tools and type systems.
This talk is organized by Tom Hurst