Wed 17 Jun 2015 17:15 - 17:40 at PLDI Main BLUE (Portland 254-255) - Synthesis II Chair(s): Isil Dillig

This paper presents an algorithm for synthesizing recursive functions that process algebraic datatypes. It is founded on proof-theoretic techniques that exploit both type information and input–output examples to prune the search space. The algorithm uses refinement trees, a data structure that succinctly represents constraints on the shape of generated code. We evaluate the algorithm by using a prototype implementation to synthesize more than 40 benchmarks and several non-trivial larger examples. The results demonstrate that the approach meets or out-performs the state-of-the-art for this domain, in terms of synthesis time or attainable size of the generated programs.

PLDI 2015 Artifact Evaluated Badge