@inproceedings{osera_type-and-example-directed_2015,
	address = {New York, NY, USA},
	series = {{PLDI} '15},
	title = {Type-and-example-directed {Program} {Synthesis}},
	isbn = {978-1-4503-3468-6},
	url = {http://doi.acm.org/10.1145/2737924.2738007},
	doi = {10/ggb9f6},
	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.},
	urldate = {2019-11-01},
	booktitle = {Proceedings of the 36th {ACM} {SIGPLAN} {Conference} on {Programming} {Language} {Design} and {Implementation}},
	publisher = {ACM},
	author = {Osera, Peter-Michael and Zdancewic, Steve},
	year = {2015},
	note = {ZSCC: 0000109 
event-place: Portland, OR, USA},
	keywords = {Functional Programming, Program Syn- thesis, Proof Search, Type Theory},
	pages = {619--630}
}

{"_id":"8SwAjwr42LXK9oYf5","bibbaseid":"osera-zdancewic-typeandexampledirectedprogramsynthesis-2015","authorIDs":[],"author_short":["Osera, P.","Zdancewic, S."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","address":"New York, NY, USA","series":"PLDI '15","title":"Type-and-example-directed Program Synthesis","isbn":"978-1-4503-3468-6","url":"http://doi.acm.org/10.1145/2737924.2738007","doi":"10/ggb9f6","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.","urldate":"2019-11-01","booktitle":"Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation","publisher":"ACM","author":[{"propositions":[],"lastnames":["Osera"],"firstnames":["Peter-Michael"],"suffixes":[]},{"propositions":[],"lastnames":["Zdancewic"],"firstnames":["Steve"],"suffixes":[]}],"year":"2015","note":"ZSCC: 0000109 event-place: Portland, OR, USA","keywords":"Functional Programming, Program Syn- thesis, Proof Search, Type Theory","pages":"619–630","bibtex":"@inproceedings{osera_type-and-example-directed_2015,\n\taddress = {New York, NY, USA},\n\tseries = {{PLDI} '15},\n\ttitle = {Type-and-example-directed {Program} {Synthesis}},\n\tisbn = {978-1-4503-3468-6},\n\turl = {http://doi.acm.org/10.1145/2737924.2738007},\n\tdoi = {10/ggb9f6},\n\tabstract = {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.},\n\turldate = {2019-11-01},\n\tbooktitle = {Proceedings of the 36th {ACM} {SIGPLAN} {Conference} on {Programming} {Language} {Design} and {Implementation}},\n\tpublisher = {ACM},\n\tauthor = {Osera, Peter-Michael and Zdancewic, Steve},\n\tyear = {2015},\n\tnote = {ZSCC: 0000109 \nevent-place: Portland, OR, USA},\n\tkeywords = {Functional Programming, Program Syn- thesis, Proof Search, Type Theory},\n\tpages = {619--630}\n}\n\n","author_short":["Osera, P.","Zdancewic, S."],"key":"osera_type-and-example-directed_2015","id":"osera_type-and-example-directed_2015","bibbaseid":"osera-zdancewic-typeandexampledirectedprogramsynthesis-2015","role":"author","urls":{"Paper":"http://doi.acm.org/10.1145/2737924.2738007"},"keyword":["Functional Programming","Program Syn- thesis","Proof Search","Type Theory"],"downloads":0},"bibtype":"inproceedings","biburl":"https://bibbase.org/zotero/k4rtik","creationDate":"2020-05-31T17:07:22.644Z","downloads":0,"keywords":["functional programming","program syn- thesis","proof search","type theory"],"search_terms":["type","example","directed","program","synthesis","osera","zdancewic"],"title":"Type-and-example-directed Program Synthesis","year":2015,"dataSources":["Z5Dp3qAJiMzxtvKMq"]}