Type-And-Example-Directed Program Synthesis
PLDI(2015)
摘要
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.
更多查看译文
关键词
Languages,Theory,Functional Programming,Proof Search,Program Synthesis,Type Theory
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络