UC San Diego

Program synthesis is a promising area of research concerned with automatically producing program implementations from high-level specifications of their behavior. Using synthesizers, programmers can write declarative and natural specifications instead of low-level implementations, and the synthesizer ensures that the resulting program does not contain errors.

The promise of synthesis is both elegant and compelling: wouldn't it be great if we didn't need to code and the compiler could magically transform a clearly, obviously correct specification into an executable implementation?

While this promise is enticing, alas there is no free lunch. Synthesis is fundamentally a search problem over the unbounded space of possible implementations. As a consequence, applications of program synthesis must bound the search space in an intelligent way, typically through clever language design of the space of possible implementations. Broadly speaking research in this field involves a tradeoff between the generality of the implementation language (i.e. how domain-specific possible programs are), and the completeness of the synthesizer (i.e. what types of programs the synthesizer can find).

In this thesis, I develop synthesizers in three different problem domains and explore the tradeoff space, from a very domain-specific and complete synthesizer to a general, domain-agnostic synthesizer that significantly restricts the space of output solutions.

In particular, I present synthesis algorithms and languages for:

1) enabling non-programmers to add interactive behavior to static diagrams;

2) inferring dynamic visual layouts from input-output examples;

3) simpler and robust imperative programs through automatically maintained data invariants.

Pleasingly in all cases, I demonstrate ways in which a synthesizer can deliver on the promise of easing and eliminating the burden of programming.