Program synthesis from polymorphic refinement types
Open Access
- 2 June 2016
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM) in ACM SIGPLAN Notices
- Vol. 51 (6), 522-538
- https://doi.org/10.1145/2908080.2908093
Abstract
We present a method for synthesizing recursive functions that provably satisfy a given specification in the form of a polymorphic refinement type. We observe that such specifications are particularly suitable for program synthesis for two reasons. First, they offer a unique combination of expressive power and decidability, which enables automatic verification—and hence synthesis—of nontrivial programs. Second, a type-based specification for a program can often be effectively decomposed into independent specifications for its components, causing the synthesizer to consider fewer component combinations and leading to a combinatorial reduction in the size of the search space. At the core of our synthesis procedure is a newalgorithm for refinement type checking, which supports specification decomposition. We have evaluated our prototype implementation on a large set of synthesis problems and found that it exceeds the state of the art in terms of both scalability and usability. The tool was able to synthesize more complex programs than those reported in prior work (several sorting algorithms and operations on balanced search trees), as well as most of the benchmarks tackled by existing synthesizers, often starting from a more concise and intuitive user input.Keywords
Other Versions
Funding Information
- Defense Advanced Research Projects Agency (FA8750-14-2-0242)
- National Science Foundation (CCF-1139056)
This publication has 40 references indexed in Scilit:
- Idris, a general-purpose dependently typed programming language: Design and implementationJournal of Functional Programming, 2013
- Recursive Program SynthesisLecture Notes in Computer Science, 2013
- Proof-Pattern Recognition and Lemma Discovery in ACL2Published by Springer Science and Business Media LLC ,2013
- Scheme-based theorem discovery and concept inventionExpert Systems with Applications, 2012
- Dependently Typed Programming in AgdaLecture Notes in Computer Science, 2009
- Hybrid type checkingACM SIGPLAN Notices, 2006
- Tridirectional typecheckingACM SIGPLAN Notices, 2004
- Intersection types and computational effectsACM SIGPLAN Notices, 2000
- Local type inferenceACM Transactions on Programming Languages and Systems, 2000
- An algorithm for type-checking dependent typesScience of Computer Programming, 1996