Example-directed synthesis: A type-theoretic interpretation

Jonathan Frankle, Peter Michael Osera, David Walker, Steve Zdancewic

Research output: Chapter in Book/Report/Conference proceedingConference contribution

20 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publicationPOPL 2016 - Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
EditorsRupak Majumdar, Rastislav Bodik
PublisherAssociation for Computing Machinery
Pages802-815
Number of pages14
ISBN (Electronic)9781450335492
DOIs
StatePublished - Jan 11 2016
Event43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016 - St. Petersburg, United States
Duration: Jan 20 2016Jan 22 2016

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
Volume20-22-January-2016
ISSN (Print)0730-8566

Other

Other43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016
CountryUnited States
CitySt. Petersburg
Period1/20/161/22/16

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • Functional programming
  • Program synthesis
  • Proof search
  • Refinement types
  • Sequent calculus
  • Type theory

Fingerprint Dive into the research topics of 'Example-directed synthesis: A type-theoretic interpretation'. Together they form a unique fingerprint.

  • Cite this

    Frankle, J., Osera, P. M., Walker, D., & Zdancewic, S. (2016). Example-directed synthesis: A type-theoretic interpretation. In R. Majumdar, & R. Bodik (Eds.), POPL 2016 - Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (pp. 802-815). (Conference Record of the Annual ACM Symposium on Principles of Programming Languages; Vol. 20-22-January-2016). Association for Computing Machinery. https://doi.org/10.1145/2837614.2837629