Wed 17 Jun 2015 17:15 - 17:40 at PLDI Main BLUE (Portland 254-255) - Synthesis II Chair(s): Işıl 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

Displayed time zone: Tijuana, Baja California change

16:00 - 17:40
Synthesis IIResearch Papers at PLDI Main BLUE (Portland 254-255)
Chair(s): Işıl Dillig University of Texas, Austin
16:00
25m
Talk
Concurrency Debugging with Differential Schedule Projections
Research Papers
Nuno Machado INESC-ID / Instituto Superior Técnico, Universidade de Lisboa, Brandon Lucia Carnegie Mellon University, Luís Rodrigues Universidade de Lisboa, Instituto Superior Técnico, INESC-ID
Media Attached
16:25
25m
Talk
Synthesis of Machine Code from Semantics
Research Papers
Venkatesh Srinivasan University of Wisconsin - Madison, Thomas Reps University of Wisconsin - Madison and Grammatech Inc.
Media Attached
16:50
25m
Talk
Synthesis of ranking functions using extremal counterexamples
Research Papers
Laure Gonnord University of Lyon & LIP, France, David Monniaux CNRS, VERIMAG, Gabriel Radanne Université Denis Diderot Paris 7, PPS
Media Attached
17:15
25m
Talk
Type-and-Example-Directed Program Synthesis
Research Papers
Peter-Michael Osera University of Pennsylvania, Steve Zdancewic
Media Attached