Sciweavers

Share
POPL
2016
ACM

Example-directed synthesis: a type-theoretic interpretation

1 years 6 months ago
Example-directed synthesis: a type-theoretic interpretation
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 s...
Jonathan Frankle, Peter-Michael Osera, David Walke
Added 09 Apr 2016
Updated 09 Apr 2016
Type Journal
Year 2016
Where POPL
Authors Jonathan Frankle, Peter-Michael Osera, David Walker, Steve Zdancewic
Comments (0)
books