---
title: "Type-and-Example-Directed Program Synthesis — Osera 2015"
description: "The paper tackles automatic generation of purely functional, recursive programs over algebraic… 27 references, cited by 13 papers here."
authors: ["Peter-Michael Osera", "Steve Zdancewic"]
year: 2015
venue: "PLDI 2015"
source: "https://www.cis.upenn.edu/~stevez/papers/OZ15.pdf"
licence: "author's copy — read only"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/osera-2015-type-example-directed-program-synthesis/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/osera-2015-type-example-directed-program-synthesis/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2015](https://md.research.elamur.ai/free/en/papers/2015/page/2/) / Type-and-Example-Directed Program Synthesis

# Type-and-Example-Directed Program Synthesis

**Authors:** Peter-Michael Osera and Steve Zdancewic · **Year:** 2015 · **Venue:** [PLDI 2015](https://md.research.elamur.ai/free/en/venues/proceedings-of-the-acm-sigplan-conference-on-programming-language-design-and/) ([Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation 2015](https://md.research.elamur.ai/free/en/venues/proceedings-of-the-acm-sigplan-conference-on-programming-language-design-and/2015/)) · **Licence:** author's copy — read only

**Links:** [Publisher's page](https://doi.org/10.1145/2737924.2738007) · [PDF](https://www.cis.upenn.edu/~stevez/papers/OZ15.pdf) · [OpenAlex](https://openalex.org/W2013596093)

**Citations:** 185 citations (OpenAlex, 2026-10-14) · [13](https://md.research.elamur.ai/free/en/papers/osera-2015-type-example-directed-program-synthesis/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## 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 Pennsylvania](https://md.research.elamur.ai/free/en/universities/university-of-pennsylvania/) — University, Philadelphia, United States · 241 works · 66,904 citations

📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🖥️ Computer Science Applications](https://md.research.elamur.ai/free/en/shelves/computer-science/computer-science-applications/) · 184 works

🧭 Topics (1): [💻 Code & programming languages](https://md.research.elamur.ai/free/en/topics/code-and-programming/) · 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.

```bibtex
@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}
}
```

- [← previous One Vector is Not Enough: Entity-Augmented Distributed Semantics for Discourse Relations](https://md.research.elamur.ai/free/en/papers/ji-2015-one-vector-is-not-enough/)
- [next → Sentiment after Translation: A Case-Study on Arabic Social Media Posts](https://md.research.elamur.ai/free/en/papers/salameh-2015-sentiment-after-translation-case-study/)
- [↑ back to papers of 2015](https://md.research.elamur.ai/free/en/papers/2015/page/2/)

## 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](https://scholar.google.com/scholar?q=Aws+Albarghouthi%2C+Sumit+Gulwani%2C+and+Zachary+Kincaid%2E+2013%2E+Recursive+Program+Synthesis%2E+In+Proceedings+of+the+25th+Conference+on+Computer%2DAided+Verification%2E)
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](https://md.research.elamur.ai/free/en/papers/alur-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](https://scholar.google.com/scholar?q=Alan+Ross+Anderson%2C+Nuel+D%2E+Belnap%2C+and+J%2E+Michael+Dunn%2E+1992%2E+Entailment%3A+The+logic+of+relevance+and+necessity%2C+vol%2E+II%2E+Princeton+University+Press%2C+Princeton%2E)
4. Lennart Augustsson. 2004. [Haskell] Announcing Djinn, version 2004-12-11, a coding wizard. [find](https://scholar.google.com/scholar?q=Lennart+Augustsson%2E+2004%2E+%5BHaskell%5D+Announcing+Djinn%2C+version+2004%2D12%2D11%2C+a+coding+wizard%2E)
5. Mailing List. (2004). [http://www.haskell.org/pipermail/haskell/2005-December/017055.html](http://www.haskell.org/pipermail/haskell/2005-December/017055.html). [↗](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](https://scholar.google.com/scholar?q=Clark+Barrett%2C+Roberto+Sebastiani%2C+Sanjit+A%2E+Seshia%2C+and+Cesare+Tinelli%2E+2008%2E+Satisfiability+Modulo+Theories%2E+IOS+Press%2E)
7. John Byrnes. 1999. Proof search and normal forms in natural deduction. Ph.D. Dissertation. Carnegie Mellon University. [find](https://scholar.google.com/scholar?q=John+Byrnes%2E+1999%2E+Proof+search+and+normal+forms+in+natural+deduction%2E+Ph%2ED%2E+Dissertation%2E+Carnegie+Mellon+University%2E)
8. Adam Chlipala. 2013. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. The MIT Press. [find](https://scholar.google.com/scholar?q=Adam+Chlipala%2E+2013%2E+Certified+Programming+with+Dependent+Types%3A+A+Pragmatic+Introduction+to+the+Coq+Proof+Assistant%2E+The+MIT+Press%2E)
9. Gerhard Gentzen. 1935. Untersuchungen uber das logische Schließen. II. Mathematische Zeitschrift 39, 1 (1935), 405–431. [find](https://scholar.google.com/scholar?q=Gerhard+Gentzen%2E+1935%2E+Untersuchungen+uber+das+logische+Schlie%C3%9Fen%2E+II%2E+Mathematische+Zeitschrift+39%2C+1+%281935%29%2C+405%E2%80%93431%2E)
10. Cordell Green. 1969. Application of Theorem Proving to Problem Solving. In International Joint Conference on Artificial Intelligence. [find](https://scholar.google.com/scholar?q=Cordell+Green%2E+1969%2E+Application+of+Theorem+Proving+to+Problem+Solving%2E+In+International+Joint+Conference+on+Artificial+Intelligence%2E)
11. Katarzyna Grygiel and Pierre Lescanne. 2013. Counting and Generating Lambda Terms. Journal of Functional Programming 23 (9 2013), 594– 628. Issue 05. [find](https://scholar.google.com/scholar?q=Katarzyna+Grygiel+and+Pierre+Lescanne%2E+2013%2E+Counting+and+Generating+Lambda+Terms%2E+Journal+of+Functional+Programming+23+%289+2013%29%2C+594%E2%80%93+628%2E+Issue+05%2E)
12. Sumit Gulwani. 2011. [Automating String Processing in Spreadsheets Using Input-output Examples](https://md.research.elamur.ai/free/en/papers/gulwani-2011-automating-string-processing-spreadsheets-input/). 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](https://scholar.google.com/scholar?q=Tihomir+Gvero%2C+Viktor+Kuncak%2C+Ivan+Kuraj%2C+and+Ruzica+Piskac%2E+2013%2E+Complete+Completion+Using+Types+and+Weights%2E+In+Proceedings+of+the+2013+ACM+SIGPLAN+Conference+on+Programming+Language+Design+and+Imp)
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](https://scholar.google.com/scholar?q=Susumu+Katayama%2E+2012%2E+An+Analytical+Inductive+Functional+Programming+System+That+Avoids+Unintended+Programs%2E+In+Proceedings+of+the+ACM+SIGPLAN+2012+Workshop+on+Partial+Evaluation+and+Program+Manipula)
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](https://scholar.google.com/scholar?q=Emanuel+Kitzelmann%2E+2010%2E+A+Combined+Analytical+and+Search%2Dbased+Approach+to+the+Inductive+Synthesis+of+Functional+Programs%2E+Ph%2ED%2E+Dissertation%2E+Fakul+at+f+ur+Wirtschafts%2Dund+Angewandte+Informatik%2C+Un)
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](https://scholar.google.com/scholar?q=Etienne+Kneuss%2C+Ivan+Kuraj%2C+Viktor+Kuncak%2C+and+Philippe+Suter%2E+2013%2E+Synthesis+Modulo+Recursive+Functions%2E+In+Proceedings+of+the+28th+ACM+SIGPLAN+on+Object%2Doriented+Programming+Systems%2C+Languages%2C+and)
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](https://scholar.google.com/scholar?q=David+Mandelin%2C+Lin+Xu%2C+Rastislav+Bod%C4%B1%CC%81k%2C+and+Doug+Kimelman%2E+2005%2E+Jungloid+Mining%3A+Helping+to+Navigate+the+API+Jungle%2E+In+Proceedings+of+the+2005+ACM+SIGPLAN+Conference+on+Programming+Language+Design)
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](https://scholar.google.com/scholar?q=Zohar+Manna+and+Richard+Waldinger%2E+1980%2E+A+Deductive+Approach+to+Program+Synthesis%2E+ACM+Trans%2E+Program%2E+Lang%2E+Syst%2E+2%2C+1+%28Jan%2E+1980%29%2C+90%E2%80%93121%2E)
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](https://scholar.google.com/scholar?q=Ulf+Norell%2E+2007%2E+Towards+a+practical+programming+language+based+on+dependent+type+theory%2E+Ph%2ED%2E+Dissertation%2E+Department+of+Computer+Science+and+Engineering%2C+Chalmers+University+of+Technology%2C+SE%2D412)
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](https://scholar.google.com/scholar?q=Daniel+Perelman%2C+Sumit+Gulwani%2C+Thomas+Ball%2C+and+Dan+Grossman%2E+2012%2E+Type%2Ddirected+Completion+of+Partial+Expressions%2E+In+Proceedings+of+the+2012+ACM+SIGPLAN+Conference+on+Programming+Language+Design+a)
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](https://scholar.google.com/scholar?q=Daniel+Perelman%2C+Sumit+Gulwani%2C+Dan+Grossman%2C+and+Peter+Provost%2E+2014%2E+Test%2Ddriven+Synthesis%2E+In+Proceedings+of+the+2014+ACM+SIGPLAN+Conference+on+Programming+Language+Design+and+Implementation+%28PLDI%29)
22. Benjamin C. Pierce and David N. Turner. 2000. Local Type Inference. ACM Trans. Program. Lang. Syst. 22, 1 (Jan. 2000), 1–44. [find](https://scholar.google.com/scholar?q=Benjamin+C%2E+Pierce+and+David+N%2E+Turner%2E+2000%2E+Local+Type+Inference%2E+ACM+Trans%2E+Program%2E+Lang%2E+Syst%2E+22%2C+1+%28Jan%2E+2000%29%2C+1%E2%80%9344%2E)
23. Armando Solar-Lezama. 2008. [Program Synthesis by Sketching](https://md.research.elamur.ai/free/en/papers/lezama-2008-program-synthesis-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](https://scholar.google.com/scholar?q=Phillip+D%2E+Summers%2E+1976%2E+A+Methodology+for+LISP+Program+Construction+From+Examples%2E+In+Proceedings+of+the+3rd+ACM+SIGACT%2DSIGPLAN+Symposium+on+Principles+of+Programming+Languages+%28POPL%29%2E)
25. The Coq Development Team. 2012. The Coq Proof Assistant: Reference Manual. INRIA, [http://coq.inria.fr/distrib/current/refman/](http://coq.inria.fr/distrib/current/refman/). [↗](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](https://scholar.google.com/scholar?q=Emina+Torlak+and+Rastislav+Bodik%2E+2014%2E+A+Lightweight+Symbolic+Virtual+Machine+for+Solver%2Daided+Host+Languages%2E+In+Proceedings+of+the+2014+ACM+SIGPLAN+Conference+on+Programming+Language+Design+and+Imp)
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](https://scholar.google.com/scholar?q=Abhishek+Udupa%2C+Arun+Raghavan%2C+Jyotirmoy+V%2E+Deshmukh%2C+Sela+Mador%2DHaim%2C+Milo+M%2EK%2E+Martin%2C+and+Rajeev+Alur%2E+2013%2E+TRANSIT%3A+Specifying+Protocols+with+Concolic+Snippets%2E+In+Proceedings+of+the+2013+ACM+SIG)

*Updated 3 November 2026*