{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:47:38Z","timestamp":1780994858317,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,1,11]],"date-time":"2016-01-11T00:00:00Z","timestamp":1452470400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"NSF","award":["CCF-1138996,CNS-1111520"],"award-info":[{"award-number":["CCF-1138996,CNS-1111520"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,1,11]]},"DOI":"10.1145\/2837614.2837629","type":"proceedings-article","created":{"date-parts":[[2016,1,7]],"date-time":"2016-01-07T09:05:00Z","timestamp":1452157500000},"page":"802-815","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":53,"title":["Example-directed synthesis: a type-theoretic interpretation"],"prefix":"10.1145","author":[{"given":"Jonathan","family":"Frankle","sequence":"first","affiliation":[{"name":"Princeton University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter-Michael","family":"Osera","sequence":"additional","affiliation":[{"name":"Grinnell College, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Walker","sequence":"additional","affiliation":[{"name":"Princeton University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Steve","family":"Zdancewic","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2016,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958069"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"e_1_3_2_1_3_1","volume-title":"Mailing List, 2004","author":"Augustsson L.","year":"2004"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1086"},{"key":"e_1_3_2_1_5_1","unstructured":"R. Davies. A practical refinement-type checker for standard ml.  R. Davies. A practical refinement-type checker for standard ml."},{"key":"e_1_3_2_1_6_1","first-page":"86","volume-title":"ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014","author":"D\u00fcdder B.","year":"2014"},{"key":"e_1_3_2_1_7_1","volume-title":"Carnegie Mellon University","author":"Dunfield J.","year":"2007"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964025"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737977"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"K. Fisher D. Walker K. Q. Zhu and P. White. From dirt to shovels: Fully automatic tool generation from ad hoc data. 2008.  K. Fisher D. Walker K. Q. Zhu and P. White. From dirt to shovels: Fully automatic tool generation from ad hoc data. 2008.","DOI":"10.1145\/1328438.1328488"},{"key":"e_1_3_2_1_11_1","unstructured":"J. Frankle. Type-directed synthesis of products Oct. 2015. URL http:\/\/arxiv.org\/abs\/1510.08121.  J. Frankle. Type-directed synthesis of products Oct. 2015. URL http:\/\/arxiv.org\/abs\/1510.08121."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/113446.113468"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926423"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462192"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103746.2103758"},{"key":"e_1_3_2_1_17_1","volume-title":"Fakul\u00e4t f\u00fcr Wirtschafts-und Angewandte Informatik","author":"Kitzelmann E.","year":"2010"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806632"},{"key":"e_1_3_2_1_19_1","volume-title":"University of Washington","author":"Lau T.","year":"2001"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594333"},{"key":"e_1_3_2_1_21_1","unstructured":"Microsoft Corporation. Microsoft by the numbers 2015. URL http: \/\/news.microsoft.com\/bythenumbers\/ms\\_numbers.pdf.  Microsoft Corporation. Microsoft by the numbers 2015. URL http: \/\/news.microsoft.com\/bythenumbers\/ms\\_numbers.pdf."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738007"},{"key":"e_1_3_2_1_23_1","unstructured":"F. Pfenning. Automated theorem proving 2004. URL http:\/\/www. cs.cmu.edu\/~fp\/courses\/atp\/index.html.  F. Pfenning. Automated theorem proving 2004. URL http:\/\/www. cs.cmu.edu\/~fp\/courses\/atp\/index.html."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"crossref","unstructured":"N. Polikarpova and A. Solar-Lezama. Program synthesis from polymorphic refinement types Oct. 2015.  N. Polikarpova and A. Solar-Lezama. Program synthesis from polymorphic refinement types Oct. 2015.","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"crossref","unstructured":"J.\n       \n      Rehof\n     and \n      \n      \n      P.\n       \n      Urzyczyn\n      \n  \n  . \n  Finite combinatory logic with intersection types. In L. Ong editor Typed Lambda Calculi and Applications volume \n  6690\n   of \n  Lecture Notes in Computer Science pages 169\u2013\n  183\n  . Springer Berlin Heidelberg 2011. ISBN 978-3-642-21690-9.. URL http:\/\/dx.doi.org\/10.1007\/978-3-642-21691-6_15.   J. Rehof and P. Urzyczyn. Finite combinatory logic with intersection types. In L. Ong editor Typed Lambda Calculi and Applications volume 6690 of Lecture Notes in Computer Science pages 169\u2013183. Springer Berlin Heidelberg 2011. ISBN 978-3-642-21690-9.. URL http:\/\/dx.doi.org\/10.1007\/978-3-642-21691-6_15.","DOI":"10.1007\/978-3-642-21691-6_15"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784757"},{"key":"e_1_3_2_1_27_1","volume-title":"University of California","author":"Solar-Lezama A.","year":"2008"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"}],"event":{"name":"POPL '16: The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"St. Petersburg FL USA","acronym":"POPL '16","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2837614.2837629","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2837614.2837629","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:43:37Z","timestamp":1750211017000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2837614.2837629"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,11]]},"references-count":27,"alternative-id":["10.1145\/2837614.2837629","10.1145\/2837614"],"URL":"https:\/\/doi.org\/10.1145\/2837614.2837629","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2914770.2837629","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2016,1,11]]},"assertion":[{"value":"2016-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}