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.
Wed 17 Jun
16:00 - 17:40: Research Papers - Synthesis II at PLDI Main BLUE (Portland 254-255) Chair(s): Isil DilligUniversity of Texas, Austin | ||||||||||||||||||||||||||||||||||||||||||
16: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 | |||||||||||||||||||||||||||||||||||||||||
16:25 - 16:50 Talk | Venkatesh SrinivasanUniversity of Wisconsin - Madison, Thomas RepsUniversity of Wisconsin - Madison and Grammatech Inc. Media Attached | |||||||||||||||||||||||||||||||||||||||||
16:50 - 17:15 Talk | Laure GonnordUniversity of Lyon & LIP, France, David MonniauxCNRS, VERIMAG, Gabriel RadanneUniversité Denis Diderot Paris 7, PPS Media Attached | |||||||||||||||||||||||||||||||||||||||||
17:15 - 17:40 Talk | Media Attached |