Program Sketching with Live Bidirectional Evaluation
We present a system called Smyth for program sketching in a typed functional language whereby the concrete evaluation of ordinary assertions gives rise to input-output examples, which are then used to guide the search to complete the holes. The key innovation, called live bidirectional evaluation, propagates examples "backward" through partially evaluated sketches. Live bidirectional evaluation enables Smyth to (a) synthesize recursive functions without trace-complete sets of examples and (b) specify and solve interdependent synthesis goals. Eliminating the trace-completeness requirement resolves a significant limitation faced by prior synthesis techniques when given partial specifications in the form of input-output examples.
To assess the practical implications of our techniques, we ran several experiments on benchmarks used to evaluate Myth, a state-of-the-art example-based synthesis tool. First, given expert examples (and no partial implementations), we find that Smyth requires on average 66% of the number of expert examples required by Myth. Second, we find that Smyth is robust to randomly-generated examples, synthesizing many tasks with relatively few more random examples than those provided by an expert. Third, we create a suite of small sketching tasks by systematically employing a simple sketching strategy to the Myth benchmarks; we find that user-provided sketches in Smyth often further reduce the total specification burden (i.e. the combination of partial implementations and examples). Lastly, we find that Leon and Synquid, two state-of-the-art logic-based synthesis tools, fail to complete several tasks on which Smyth succeeds.
Thu 21 OctDisplayed time zone: Central Time (US & Canada) change
10:50 - 12:10
|A General Approach to Define Binders using Matching Logic
Xiaohong Chen University of Illinois at Urbana-Champaign, Grigore Roşu University of Illinois at Urbana-ChampaignDOI
|Denotational Recurrence Extraction for Amortized Analysis
Joseph W. Cutler University of Pennsylvania, Daniel R. Licata Wesleyan University, Norman Danner Wesleyan UniversityDOI
|Program Sketching with Live Bidirectional Evaluation
Justin Lubin University of California at Berkeley, Nick Collins University of Chicago, Cyrus Omar University of Michigan, Ravi Chugh University of ChicagoDOI
|Liquid Information Flow Control
Nadia Polikarpova University of California at San Diego, Jean Yang Carnegie Mellon University, Deian Stefan University of California at San Diego, USA, Shachar Itzhaky Technion, Armando Solar-Lezama Massachusetts Institute of Technology, Travis Hance Carnegie Mellon UniversityDOI
|Discussion, Questions and Answers