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

Wed 17 Jun

pldi2015-papers
16:00 - 17:40: Research Papers - Synthesis II at PLDI Main BLUE (Portland 254-255)
Chair(s): Isil DilligUniversity of Texas, Austin
pldi2015-papers16:00 - 16:25
Talk
Nuno MachadoINESC-ID / Instituto Superior Técnico, Universidade de Lisboa, Brandon LuciaCarnegie Mellon University, Luís RodriguesUniversidade de Lisboa, Instituto Superior Técnico, INESC-ID
Media Attached
pldi2015-papers16:25 - 16:50
Talk
Venkatesh SrinivasanUniversity of Wisconsin - Madison, Thomas RepsUniversity of Wisconsin - Madison and Grammatech Inc.
Media Attached
pldi2015-papers16:50 - 17:15
Talk
Laure GonnordUniversity of Lyon & LIP, France, David MonniauxCNRS, VERIMAG, Gabriel RadanneUniversité Denis Diderot Paris 7, PPS
Media Attached
pldi2015-papers17:15 - 17:40
Talk
Peter-Michael OseraUniversity of Pennsylvania, Steve Zdancewic
Media Attached