Type-and-example-directed program synthesis
Top Cited Papers
- 3 June 2015
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM)
Abstract
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. Our results demonstrate that the approach meets or outperforms the state-of-the-art for this domain, in terms of synthesis time or attainable size of the generated programs.Keywords
This publication has 21 references indexed in Scilit:
- A lightweight symbolic virtual machine for solver-aided host languagesACM SIGPLAN Notices, 2014
- Test-driven synthesisACM SIGPLAN Notices, 2014
- Synthesis modulo recursive functionsPublished by Association for Computing Machinery (ACM) ,2013
- Complete completion using types and weightsPublished by Association for Computing Machinery (ACM) ,2013
- Recursive Program SynthesisLecture Notes in Computer Science, 2013
- A Combined Analytical and Search-Based Approach for the Inductive Synthesis of Functional ProgramsKI - Künstliche Intelligenz, 2010
- Local type inferenceACM Transactions on Programming Languages and Systems, 2000
- A Deductive Approach to Program SynthesisACM Transactions on Programming Languages and Systems, 1980
- A methodology for LISP program construction from examplesPublished by Association for Computing Machinery (ACM) ,1976
- Untersuchungen ber das logische Schlie en. IIMathematische Zeitschrift, 1935