CAREER: Type-Driven Program Synthesis

University Of California-San Diego, La Jolla CA

Investigators

Abstract

It is becoming increasingly important to automate low-level aspects of programming to help developers increase productivity and avoid mistakes. Program synthesis is an emerging technology for automatically generating programs from high-level descriptions of the task they must perform. Making program synthesis practical requires addressing two major challenges:(1) how should the programmer communicate their intent to the synthesizer? and (2) how does one efficiently search the space of all programs the synthesizer needs to consider? The Type-Driven Synthesis project (TyDriS) tackles both of these challenges using a novel type-based approach, which leverages decades of work on type systems from the Programming Languages community for the benefit of program synthesis. Towards the challenge of specification, TyDriS contributes powerful languages that allow the programmer to communicate a lot of information very concisely, and get relevant results even in the presence of ambiguity. Towards the challenge of scale, TyDriS contributes new search algorithms that allow synthesis to leverage large code libraries and integrate synthesized code with programmer-written code. These innovations enable three novel applications: a library-based synthesizer for Haskell, a privacy-aware web framework, and a synthesis-aided programming tutor. 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.