research-article

Open access

Type-and-example-directed program synthesis

Authors:

Peter-Michael Osera,

Steve ZdancewicAuthors Info & Claims

PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 619 - 630

https://doi.org/10.1145/2737924.2738007

Published: 03 June 2015 Publication History

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.

References

[1]

Aws Albarghouthi, Sumit Gulwani, and Zachary Kincaid. 2013. Recursive Program Synthesis. In Proceedings of the 25th Conference on Computer-Aided Verification.

Digital Library

[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. Syntaxguided 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.

[4]

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.

[5]

Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. 2008. Satisfiability Modulo Theories. IOS Press.

[6]

John Byrnes. 1999. Proof search and normal forms in natural deduction. Ph.D. Dissertation. Carnegie Mellon University.

[7]

Adam Chlipala. 2013. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. The MIT Press.

Digital Library

[8]

Gerhard Gentzen. 1935. Untersuchungen uber das logische Schließen. II. Mathematische Zeitschrift 39, 1 (1935), 405–431.

[9]

Cordell Green. 1969. Application of Theorem Proving to Problem Solving. In International Joint Conference on Artificial Intelligence.

Digital Library

[10]

Katarzyna Grygiel and Pierre Lescanne. 2013. Counting and Generating Lambda Terms. Journal of Functional Programming 23 (9 2013), 594–628. Issue 05.

[11]

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).

Digital Library

[12]

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).

Digital Library

[13]

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.

Digital Library

[14]

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.

[15]

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).

Digital Library

[16]

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).

Digital Library

[17]

Zohar Manna and Richard Waldinger. 1980. A Deductive Approach to Program Synthesis. ACM Trans. Program. Lang. Syst. 2, 1 (Jan. 1980), 90–121.

Digital Library

[18]

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.

[19]

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).

Digital Library

[20]

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).

Digital Library

[21]

Benjamin C. Pierce and David N. Turner. 2000. Local Type Inference. ACM Trans. Program. Lang. Syst. 22, 1 (Jan. 2000), 1–44.

Digital Library

[22]

Armando Solar-Lezama. 2008. Program Synthesis by Sketching. Ph.D. Dissertation. University of California, Berkeley.

Digital Library

[23]

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).

Digital Library

[24]

The Coq Development Team. 2012. The Coq Proof Assistant: Reference Manual. INRIA, http://coq.inria.fr/distrib/current/refman/.

[25]

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).

Digital Library

Cited By

Xia JLiu JBrown NChen YFeng YFilkov VRay BZhou M(2024)Refinement Types for VisualizationProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695550(1871-1881)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695550
Mulleners NJeuring JHeeren B(2024)Example-Based Reasoning about the Realizability of Polymorphic ProgramsProceedings of the ACM on Programming Languages10.1145/36746368:ICFP(317-337)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674636
Lubin JFerguson JYe KYim JChasins S(2024)Equivalence by Canonicalization for Synthesis-Backed RefactoringProceedings of the ACM on Programming Languages10.1145/36564538:PLDI(1879-1904)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656453
Show More Cited By

Index Terms

Type-and-example-directed program synthesis
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
2. Theory of computation

Recommendations

Type-and-example-directed program synthesis
PLDI '15

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 ...
Program synthesis from polymorphic refinement types
PLDI '16: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation

We 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 Languages

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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2015

630 pages

ISBN:9781450334686

DOI:10.1145/2737924

General Chair:
David Grove
IBM Research, USA
,
Program Chair:
Steve Blackburn
Australian National University, Australia

ACM SIGPLAN Notices Volume 50, Issue 6
PLDI '15
June 2015
630 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2813885
Editor:
Andy Gill
University of Kansas, Lawrence, KS
Issue’s Table of Contents

Copyright © 2015 Owner/Author.

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 03 June 2015

Check for updates

Author Tags

Qualifiers

Research-article

Conference

PLDI '15

Sponsor:

SIGPLAN

PLDI '15: ACM SIGPLAN Conference on Programming Language Design and Implementation

June 13 - 17, 2015

OR, Portland, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

151
Total Citations
View Citations
3,410
Total Downloads

Downloads (Last 12 months)396
Downloads (Last 6 weeks)59

Reflects downloads up to 05 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Xia JLiu JBrown NChen YFeng YFilkov VRay BZhou M(2024)Refinement Types for VisualizationProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695550(1871-1881)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695550
Mulleners NJeuring JHeeren B(2024)Example-Based Reasoning about the Realizability of Polymorphic ProgramsProceedings of the ACM on Programming Languages10.1145/36746368:ICFP(317-337)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674636
Lubin JFerguson JYe KYim JChasins S(2024)Equivalence by Canonicalization for Synthesis-Backed RefactoringProceedings of the ACM on Programming Languages10.1145/36564538:PLDI(1879-1904)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656453
Li STheodoridis TSu Z(2024)Boosting Compiler Testing by Injecting Real-World CodeProceedings of the ACM on Programming Languages10.1145/36563868:PLDI(223-245)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656386
Ji RZhao YXiong YWang DZhang LHu Z(2024)Decomposition-based Synthesis for Applying Divide-and-Conquer-like Algorithmic ParadigmsACM Transactions on Programming Languages and Systems10.1145/364844046:2(1-59)Online publication date: 17-Jun-2024
https://dl.acm.org/doi/10.1145/3648440
Frank JQuiring BLampropoulos L(2024)Generating Well-Typed Terms That Are Not “Useless”Proceedings of the ACM on Programming Languages10.1145/36329198:POPL(2318-2339)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632919
Ding YQiu X(2024)Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector ManipulationsProceedings of the ACM on Programming Languages10.1145/36329138:POPL(2129-2159)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632913
Nazari ASwayamdipta SChattopadhyay SRaghothaman M(2024)Generating Function Names to Improve Comprehension of Synthesized Programs2024 IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC)10.1109/VL/HCC60511.2024.00035(248-259)Online publication date: 2-Sep-2024
https://doi.org/10.1109/VL/HCC60511.2024.00035
Miltner AWang ZChaudhuri SDillig I(2024)Relational Synthesis of Recursive Programs via Constraint Annotated Tree AutomataComputer Aided Verification10.1007/978-3-031-65633-0_3(41-63)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65633-0_3
Nazari AHuang YSamanta RRadhakrishna ARaghothaman M(2023)Explainable Program Synthesis by Localizing SpecificationsProceedings of the ACM on Programming Languages10.1145/36228747:OOPSLA2(2171-2195)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622874
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents