Tue 16 Jun 2015 10:30 - 10:55 at PLDI Main RED (Portland 256) - Synthesis I Chair(s): Kathleen Fisher

We present a method for example-guided synthesis of functional programs over recursive data structures. Given a set of input-output examples, our method synthesizes a program in a functional language with higher-order combinators like map and fold. The synthesized program is guaranteed to be the simplest program in the language to fit the examples.

Our approach combines three technical ideas: inductive generalization, deduction, and enumerative search. First, we generalize the input-output examples into hypotheses about the structure of the target program. For each hypothesis, we use deduction to infer new input/output examples for the missing subexpressions. This leads to a new subproblem where the goal is to synthesize expressions within each hypothesis. Since not every hypothesis can be realized into a program that fits the examples, we use a combination of best-first enumeration and deduction to search for a hypothesis that meets our needs.

We have implemented our method in a tool called Lambda^2, and we evaluate this tool on a large set of synthesis problems involving lists, trees, and nested data structures. The experiments demonstrate the scalability and broad scope of Lambda^2. A highlight is the synthesis of a program believed to be the world’s earliest functional pearl.

Tue 16 Jun
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

09:15 - 10:55: Research Papers - Synthesis I at PLDI Main RED (Portland 256)
Chair(s): Kathleen FisherTufts University
pldi2015-papers09:15 - 09:40
Jedidiah McClurgUniversity of Colorado Boulder, Hossein HojjatCornell University, Pavol CernyUniversity of Colorado Boulder, Nate FosterCornell University
Pre-print Media Attached
pldi2015-papers09:40 - 10:05
Aditya NoriMicrosoft Research, UK, Sherjil OzairIIT Delhi, Sriram RajamaniMicrosoft Research, Deepak VijaykeerthyMicrosoft Research
Media Attached
pldi2015-papers10:05 - 10:30
Dan BarowyUniversity of Massachusetts Amherst, Sumit GulwaniMicrosoft Research, Ted HartMicrosoft Research, Benjamin ZornMicrosoft Research
Media Attached
pldi2015-papers10:30 - 10:55
John FeserRice University, Swarat ChaudhuriRice University, Isil DilligUniversity of Texas, Austin
Media Attached