Peter-Michael Osera
Steve Zdancewic
ABSTRACT
This paper presents an algorithm for synthesizing recursive functions that process algebraic datatypes. It is founded on proof-theoretic techniques that exploit both type information and input–output examples to prune the search space. The algorithm uses refinement trees, a data structure that succinctly represents constraints on the shape of generated code. We evaluate the algorithm by using a prototype implementation to synthesize more than 40 benchmarks and several non-trivial larger examples. Our results demonstrate that the approach meets or outperforms the state-of-the-art for this domain, in terms of synthesis time or attainable size of the generated programs.
- Aws Albarghouthi, Sumit Gulwani, and Zachary Kincaid. 2013. Recursive Program Synthesis. In Proceedings of the 25th Conference on Computer-Aided Verification. Google Scholar
Digital Library
- 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. Syntaxguided Synthesis. In 13th International Conference on Formal Methods in Computer-aided Design.Google Scholar
- Alan Ross Anderson, Nuel D. Belnap, and J. Michael Dunn. 1992. Entailment: The logic of relevance and necessity, vol. II. Princeton University Press, Princeton.Google ScholarCross Ref
- Lennart Augustsson. 2004. {Haskell} Announcing Djinn, version 2004-12-11, a coding wizard. Mailing List. (2004). http://www.haskell.org/pipermail/haskell/ 2005-December/017055.html.Google Scholar
- Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. 2008. Satisfiability Modulo Theories. IOS Press.Google Scholar
- John Byrnes. 1999. Proof search and normal forms in natural deduction. Ph.D. Dissertation. Carnegie Mellon University.Google Scholar
- Adam Chlipala. 2013. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. The MIT Press. Google ScholarDigital Library
- Gerhard Gentzen. 1935. Untersuchungen uber das logische Schließen. II. Mathematische Zeitschrift 39, 1 (1935), 405–431.Google ScholarCross Ref
- Cordell Green. 1969. Application of Theorem Proving to Problem Solving. In International Joint Conference on Artificial Intelligence. Google ScholarDigital Library
- Katarzyna Grygiel and Pierre Lescanne. 2013. Counting and Generating Lambda Terms. Journal of Functional Programming 23 (9 2013), 594–628. Issue 05.Google Scholar
- 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). Google ScholarDigital Library
- 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). Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google Scholar
- 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). Google ScholarDigital Library
- 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). Google ScholarDigital Library
- Zohar Manna and Richard Waldinger. 1980. A Deductive Approach to Program Synthesis. ACM Trans. Program. Lang. Syst. 2, 1 (Jan. 1980), 90–121. Google ScholarDigital Library
- 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.Google Scholar
- 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). Google ScholarDigital Library
- 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). Google ScholarDigital Library
- Benjamin C. Pierce and David N. Turner. 2000. Local Type Inference. ACM Trans. Program. Lang. Syst. 22, 1 (Jan. 2000), 1–44. Google ScholarDigital Library
- Armando Solar-Lezama. 2008. Program Synthesis by Sketching. Ph.D. Dissertation. University of California, Berkeley. Google ScholarDigital Library
- Phillip D. Summers. 1976. A Methodology for LISP Program Construction From Examples. In Proceedings of the 3rd ACM SIGACTSIGPLAN Symposium on Principles of Programming Languages (POPL). Google ScholarDigital Library
- The Coq Development Team. 2012. The Coq Proof Assistant: Reference Manual. INRIA, http://coq.inria.fr/distrib/current/refman/.Google Scholar
- 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). Google ScholarDigital Library
Index Terms
- Type-and-example-directed program synthesis
Recommendations
Type-and-example-directed program synthesis
PLDI '15This paper presents an algorithm for synthesizing recursive functions that process algebraic datatypes. It is founded on proof-theoretic techniques that exploit both type information and input–output examples to prune the search space. The algorithm ...
Program synthesis from polymorphic refinement types
PLDI '16: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and ImplementationWe 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. ...
Example-directed synthesis: a type-theoretic interpretation
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesInput-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 ...
Comments