TY - JOUR
T1 - Example-directed synthesis
T2 - A type-theoretic interpretation
AU - Frankle, Jonathan
AU - Osera, Peter Michael
AU - Walker, David
AU - Zdancewic, Steve
N1 - Funding Information:
We would like to thank the anonymous reviewers for their comments and feedback on our work. This work was supported in part by the NSF under awards CCF-1138996 and CNS-1111520.
Publisher Copyright:
© 2016 ACM.
PY - 2016/4/8
Y1 - 2016/4/8
N2 - Input-output examples have emerged as a practical and user-friendly specification mechanism for program synthesis in many environments. While example-driven tools have demonstrated tangible impact that has inspired adoption in industry, their underlying semantics are less well-understood: what are "examples" and how do they relate to other kinds of specifications? This paper demonstrates that examples can, in general, be interpreted as refinement types. Seen in this light, program synthesis is the task of finding an inhabitant of such a type. This insight provides an immediate semantic interpretation for examples. Moreover, it enables us to exploit decades of research in type theory as well as its correspondence with intuitionistic logic rather than designing ad hoc theoretical frameworks for synthesis from scratch. We put this observation into practice by formalizing synthesis as proof search in a sequent calculus with intersection and union refinements that we prove to be sound with respect to a conventional type system. In addition, we show how to handle negative examples, which arise from user feedback or counterexample-guided loops. This theory serves as the basis for a prototype implementation that extends our core language to support ML-style algebraic data types and structurally inductive functions. Users can also specify synthesis goals using polymorphic refinements and import monomorphic libraries. The prototype serves as a vehicle for empirically evaluating a number of different strategies for resolving the nondeterminism of the sequent calculus-bottom-up theorem-proving, term enumeration with refinement type checking, and combinations of both-the results of which classify, explain, and validate the design choices of existing synthesis systems. It also provides a platform for measuring the practical value of a specification language that combines "examples" with the more general expressiveness of refinements.
AB - Input-output examples have emerged as a practical and user-friendly specification mechanism for program synthesis in many environments. While example-driven tools have demonstrated tangible impact that has inspired adoption in industry, their underlying semantics are less well-understood: what are "examples" and how do they relate to other kinds of specifications? This paper demonstrates that examples can, in general, be interpreted as refinement types. Seen in this light, program synthesis is the task of finding an inhabitant of such a type. This insight provides an immediate semantic interpretation for examples. Moreover, it enables us to exploit decades of research in type theory as well as its correspondence with intuitionistic logic rather than designing ad hoc theoretical frameworks for synthesis from scratch. We put this observation into practice by formalizing synthesis as proof search in a sequent calculus with intersection and union refinements that we prove to be sound with respect to a conventional type system. In addition, we show how to handle negative examples, which arise from user feedback or counterexample-guided loops. This theory serves as the basis for a prototype implementation that extends our core language to support ML-style algebraic data types and structurally inductive functions. Users can also specify synthesis goals using polymorphic refinements and import monomorphic libraries. The prototype serves as a vehicle for empirically evaluating a number of different strategies for resolving the nondeterminism of the sequent calculus-bottom-up theorem-proving, term enumeration with refinement type checking, and combinations of both-the results of which classify, explain, and validate the design choices of existing synthesis systems. It also provides a platform for measuring the practical value of a specification language that combines "examples" with the more general expressiveness of refinements.
KW - Functional programming
KW - Program synthesis
KW - Proof search
KW - Refinement types
KW - Sequent calculus
KW - Type theory
UR - http://www.scopus.com/inward/record.url?scp=84965043058&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84965043058&partnerID=8YFLogxK
U2 - 10.1145/2837614.2837629
DO - 10.1145/2837614.2837629
M3 - Article
AN - SCOPUS:84965043058
SN - 1523-2867
VL - 51
SP - 802
EP - 815
JO - SIGPLAN Notices (ACM Special Interest Group on Programming Languages)
JF - SIGPLAN Notices (ACM Special Interest Group on Programming Languages)
IS - 1
ER -