Elamur Research⌕
☰
home / papers / 2015 / Type-and-Example-Directed Program Synthesis

Type-and-Example-Directed Program Synthesis

Paper · 2015 · Peter-Michael Osera and Steve Zdancewic

Summary

The paper tackles automatic generation of purely functional, recursive programs over algebraic datatypes. The specification is a goal type plus a handful of input–output examples. The authors revisit the classic view of synthesis as proof search and add a key twist: examples are threaded through the typing rules alongside types. They are distributed into constructor arguments, match branches and recursive calls, so candidate subterms can be checked against examples while the program is still being built. Checking happens during enumeration, not only after a full candidate exists. The formal calculus, λsyn, is turned into an algorithm through a "refinement tree" data structure, which captures the code shape shared by many candidates. A guessing procedure restricted to β-normal terms fills the remaining holes. The prototype, MYTH, targets a subset of OCaml. On over 40 benchmarks and several larger programs, it matched or beat Escher and Leon in synthesis time or in the size of programs it could produce. This suggests that type structure is a strong lever for example-driven synthesis.

Key points

  • Search is limited to well-typed, structurally recursive terms in β-normal, η-long form. A proof-relevance optimization further speeds up the implementation.
  • Pushing examples inward splits a search over a constructor like Cons(e1, e2) into independent subproblems. This cuts interpreter calls from roughly N1 × N2 to N1 + N2.
  • For recursive functions, the user's examples act as a partial-function approximation of the recursive call. This lets MYTH synthesize the stutter list function in about 0.001 s.
  • Unlike prior tools, MYTH can synthesize higher-order functions such as map and fold, use higher-order functions, and handle large algebraic datatypes. It sometimes finds unexpected "inside-out" recursive solutions because they save an AST node.
  • Compared to related systems: Escher builds terms bottom-up, while MYTH works top-down. Leon relies on CEGIS and an SMT solver with properties rather than examples. The work was funded by NSF ExCAPE (CCF-1138996).

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓University of PennsylvaniaPhiladelphia · United States241 works · 66,904 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputer Science Applications · 184 works

🧭 Topics 1Research subjects and languages the work is about.Code & programming languages · 194 works

Cite

Cite as Peter-Michael Osera and Steve Zdancewic. 2015. Type-and-Example-Directed Program Synthesis. PLDI 2015.

The paper itself, not this page. BibTeX from the library's record of the work.

@inproceedings{osera2015type,
  title = {{Type-and-Example-Directed Program Synthesis}},
  author = {Peter-Michael Osera and Steve Zdancewic},
  booktitle = {PLDI 2015},
  year = {2015},
  doi = {10.1145/2737924.2738007},
  url = {https://doi.org/10.1145/2737924.2738007}
}

References

27 references, 3 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Aws Albarghouthi, Sumit Gulwani, and Zachary Kincaid. 2013. Recursive Program Synthesis. In Proceedings of the 25th Conference on Computer-Aided Verification. find
  2. Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishk Udupa. 2013. Syntax-guided Synthesis. In 13th International Conference on Formal Methods in Computer-aided Design.
  3. Alan Ross Anderson, Nuel D. Belnap, and J. Michael Dunn. 1992. Entailment: The logic of relevance and necessity, vol. II. Princeton University Press, Princeton. find
  4. Lennart Augustsson. 2004. [Haskell] Announcing Djinn, version 2004-12-11, a coding wizard. find
  5. Mailing List. (2004). http://www.haskell.org/pipermail/haskell/2005-December/017055.html. ↗
  6. Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. 2008. Satisfiability Modulo Theories. IOS Press. find
  7. John Byrnes. 1999. Proof search and normal forms in natural deduction. Ph.D. Dissertation. Carnegie Mellon University. find
  8. Adam Chlipala. 2013. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. The MIT Press. find
  9. Gerhard Gentzen. 1935. Untersuchungen uber das logische Schließen. II. Mathematische Zeitschrift 39, 1 (1935), 405–431. find
  10. Cordell Green. 1969. Application of Theorem Proving to Problem Solving. In International Joint Conference on Artificial Intelligence. find
  11. Katarzyna Grygiel and Pierre Lescanne. 2013. Counting and Generating Lambda Terms. Journal of Functional Programming 23 (9 2013), 594– 628. Issue 05. find
  12. Sumit Gulwani. 2011. Automating String Processing in Spreadsheets Using Input-output Examples. In Proceedings of the 38th Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL).
  13. Tihomir Gvero, Viktor Kuncak, Ivan Kuraj, and Ruzica Piskac. 2013. Complete Completion Using Types and Weights. In Proceedings of the 2013 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). find
  14. Susumu Katayama. 2012. An Analytical Inductive Functional Programming System That Avoids Unintended Programs. In Proceedings of the ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation (PEPM ’12). ACM, New York, NY, USA, 43–52. find
  15. Emanuel Kitzelmann. 2010. A Combined Analytical and Search-based Approach to the Inductive Synthesis of Functional Programs. Ph.D. Dissertation. Fakul at f ur Wirtschafts-und Angewandte Informatik, Universit at Bamberg. find
  16. Etienne Kneuss, Ivan Kuraj, Viktor Kuncak, and Philippe Suter. 2013. Synthesis Modulo Recursive Functions. In Proceedings of the 28th ACM SIGPLAN on Object-oriented Programming Systems, Languages, and Applications (OOPSLA). find
  17. David Mandelin, Lin Xu, Rastislav Bodı́k, and Doug Kimelman. 2005. Jungloid Mining: Helping to Navigate the API Jungle. In Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). find
  18. Zohar Manna and Richard Waldinger. 1980. A Deductive Approach to Program Synthesis. ACM Trans. Program. Lang. Syst. 2, 1 (Jan. 1980), 90–121. find
  19. Ulf Norell. 2007. Towards a practical programming language based on dependent type theory. Ph.D. Dissertation. Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden. find
  20. Daniel Perelman, Sumit Gulwani, Thomas Ball, and Dan Grossman. 2012. Type-directed Completion of Partial Expressions. In Proceedings of the 2012 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). find
  21. Daniel Perelman, Sumit Gulwani, Dan Grossman, and Peter Provost. 2014. Test-driven Synthesis. In Proceedings of the 2014 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). find
  22. Benjamin C. Pierce and David N. Turner. 2000. Local Type Inference. ACM Trans. Program. Lang. Syst. 22, 1 (Jan. 2000), 1–44. find
  23. Armando Solar-Lezama. 2008. Program Synthesis by Sketching. Ph.D. Dissertation. University of California, Berkeley.
  24. Phillip D. Summers. 1976. A Methodology for LISP Program Construction From Examples. In Proceedings of the 3rd ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL). find
  25. The Coq Development Team. 2012. The Coq Proof Assistant: Reference Manual. INRIA, http://coq.inria.fr/distrib/current/refman/. ↗
  26. Emina Torlak and Rastislav Bodik. 2014. A Lightweight Symbolic Virtual Machine for Solver-aided Host Languages. In Proceedings of the 2014 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). find
  27. Abhishek Udupa, Arun Raghavan, Jyotirmoy V. Deshmukh, Sela Mador-Haim, Milo M.K. Martin, and Rajeev Alur. 2013. TRANSIT: Specifying Protocols with Concolic Snippets. In Proceedings of the 2013 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/osera-2015-type-example-directed-program-synthesis/