SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
Thu 21 Oct 2021 11:20 - 11:35 at Zurich E - ICFP 2020 Papers Chair(s): Stefan K. Muller

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 Oct

Displayed time zone: Central Time (US & Canada) change

10:50 - 12:10
ICFP 2020 PapersSIGPLAN Papers at Zurich E
Chair(s): Stefan K. Muller Illinois Institute of Technology
10:50
15m
Talk
A General Approach to Define Binders using Matching Logic
SIGPLAN Papers
Xiaohong Chen University of Illinois at Urbana-Champaign, Grigore Ro┼ču University of Illinois at Urbana-Champaign
DOI
11:05
15m
Talk
Denotational Recurrence Extraction for Amortized Analysis
SIGPLAN Papers
Joseph W. Cutler University of Pennsylvania, Dan Licata Wesleyan University, Norman Danner Wesleyan University
DOI
11:20
15m
Talk
Program Sketching with Live Bidirectional Evaluation
SIGPLAN Papers
Justin Lubin University of California at Berkeley, Nick Collins University of Chicago, Cyrus Omar University of Michigan, Ravi Chugh University of Chicago
DOI
11:35
15m
Talk
Liquid Information Flow Control
SIGPLAN Papers
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 University
DOI
11:50
20m
Live Q&A
Discussion, Questions and Answers
SIGPLAN Papers