{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:43:46Z","timestamp":1767926626902,"version":"3.49.0"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1814358, 1911149"],"award-info":[{"award-number":["1814358, 1911149"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,1]]},"abstract":"<jats:p>\n            We consider the problem of type-directed component-based synthesis where, given a set of (typed) components and a query\n            <jats:italic>type<\/jats:italic>\n            , the goal is to synthesize a\n            <jats:italic>term<\/jats:italic>\n            that inhabits the query. Classical approaches based on proof search in intuitionistic logics do not scale up to the standard libraries of modern languages, which span hundreds or thousands of components. Recent graph reachability based methods proposed for Java do scale, but only apply to monomorphic data and components: polymorphic data and components infinitely explode the size of the graph that must be searched, rendering synthesis intractable. We introduce\n            <jats:italic>type-guided abstraction refinement<\/jats:italic>\n            (TYGAR), a new approach for scalable type-directed synthesis over polymorphic datatypes and components. Our key insight is that we can overcome the explosion by building a graph over\n            <jats:italic>abstract types<\/jats:italic>\n            which represent a potentially unbounded set of concrete types. We show how to use graph reachability to search for candidate terms over abstract types, and introduce a new algorithm that uses\n            <jats:italic>proofs of untypeability<\/jats:italic>\n            of ill-typed candidates to iteratively\n            <jats:italic>refine<\/jats:italic>\n            the abstraction until a well-typed result is found.\n          <\/jats:p>\n          <jats:p>We have implemented TYGAR in H+, a tool that takes as input a set of Haskell libraries and a query type, and returns a Haskell term that uses functions from the provided libraries to implement the query type. Our support for polymorphism allows H+ to work with higher-order functions and type classes, and enables more precise queries due to parametricity. We have evaluated H+ on 44 queries using a set of popular Haskell libraries with a total of 291 components. H+ returns an interesting solution within the first five results for 32 out of 44 queries. Our results show that TYGAR allows H+ to rapidly return well-typed terms, with the median time to first solution of just 1.4 seconds. Moreover, we observe that gains from iterative refinement over exhaustive enumeration are more pronounced on harder queries.<\/jats:p>","DOI":"10.1145\/3371080","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":34,"title":["Program synthesis by type-guided abstraction refinement"],"prefix":"10.1145","volume":"4","author":[{"given":"Zheng","family":"Guo","sequence":"first","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"James","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Justo","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jiaxiao","family":"Zhou","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ziteng","family":"Wang","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ranjit","family":"Jhala","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nadia","family":"Polikarpova","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_18"},{"key":"e_1_2_2_2_1","unstructured":"Lennart Augusstson. 2005. Djinn. https:\/\/github.com\/augustss\/djinn .  Lennart Augusstson. 2005. Djinn. https:\/\/github.com\/augustss\/djinn ."},{"key":"e_1_2_2_3_1","volume-title":"The lambda calculus - its syntax and semantics. Studies in logic and the foundations of mathematics","author":"Barendregt Hendrik Pieter","unstructured":"Hendrik Pieter Barendregt . 1985. The lambda calculus - its syntax and semantics. Studies in logic and the foundations of mathematics , Vol. 103 . North-Holland . Hendrik Pieter Barendregt. 1985. The lambda calculus - its syntax and semantics. Studies in logic and the foundations of mathematics, Vol. 103. North-Holland."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13754-9_4"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263744"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_7_1","volume-title":"TACAS (LNCS)","author":"de Moura Leonardo Mendon\u00e7a","unstructured":"Leonardo Mendon\u00e7a de Moura and Nikolaj Bj\u00f8rner . 2008. Z3: An Efficient SMT Solver . In TACAS (LNCS) , Vol. 4963 . Springer , 337\u2013340. Leonardo Mendon\u00e7a de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In TACAS (LNCS), Vol. 4963. Springer, 337\u2013340."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000861"},{"key":"e_1_2_2_9_1","volume-title":"Sets and proofs","author":"Dyckhoff Roy","unstructured":"Roy Dyckhoff and Lu\u00eds Pinto . 1998. Proof Search in Constructive Logics . In In Sets and proofs . Cambridge University Press , 53\u201365. Roy Dyckhoff and Lu\u00eds Pinto. 1998. Proof Search in Constructive Logics. In In Sets and proofs. Cambridge University Press, 53\u201365."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_40"},{"key":"e_1_2_2_11_1","volume-title":"Reps","author":"Feng Yu","year":"2017","unstructured":"Yu Feng , Ruben Martins , Yuepeng Wang , Isil Dillig , and Thomas W . Reps . 2017 . Component-based synthesis for complex APIs. In POPL. Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, and Thomas W. Reps. 2017. Component-based synthesis for complex APIs. In POPL."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837629"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568250"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73094-1_10"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837670"},{"key":"e_1_2_2_16_1","doi-asserted-by":"crossref","unstructured":"Susanne Graf and Hassen Saidi. 1997. Construction of abstract state graphs with PVS. In Computer Aided Verification. 72\u201383.  Susanne Graf and Hassen Saidi. 1997. Construction of abstract state graphs with PVS. In Computer Aided Verification. 72\u201383.","DOI":"10.1007\/3-540-63166-6_10"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926423"},{"key":"e_1_2_2_18_1","volume-title":"Program Synthesis by Type-Guided Abstraction Refinement. arXiv","author":"Guo Zheng","year":"1911","unstructured":"Zheng Guo , Michael James , David Justo , Jiaxiao Zhou , Ziteng Wang , Ranjit Jhala , and Nadia Polikarpova . 2019. Program Synthesis by Type-Guided Abstraction Refinement. arXiv : 1911 .04091 Zheng Guo, Michael James, David Justo, Jiaxiao Zhou, Ziteng Wang, Ranjit Jhala, and Nadia Polikarpova. 2019. Program Synthesis by Type-Guided Abstraction Refinement. arXiv: 1911.04091"},{"key":"e_1_2_2_19_1","doi-asserted-by":"crossref","unstructured":"Tihomir Gvero Viktor Kuncak Ivan Kuraj and Ruzica Piskac. 2013. Complete completion using types and weights. In PLDI.  Tihomir Gvero Viktor Kuncak Ivan Kuraj and Ruzica Piskac. 2013. Complete completion using types and weights. In PLDI.","DOI":"10.1145\/2491956.2462192"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47166-2_21"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103746.2103758"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_10"},{"key":"e_1_2_2_23_1","unstructured":"Woosuk Lee Kihong Heo Rajeev Alur and Mayur Naik. 2018. Accelerating Search-based Program Synthesis Using Learned Probabilistic Models. In PLDI.  Woosuk Lee Kihong Heo Rajeev Alur and Mayur Naik. 2018. Accelerating Search-based Program Synthesis Using Learned Probabilistic Models. In PLDI."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065018"},{"key":"e_1_2_2_25_1","unstructured":"Neil Mitchell. 2004. Hoogle. https:\/\/www.haskell.org\/hoogle\/ .  Neil Mitchell. 2004. Hoogle. https:\/\/www.haskell.org\/hoogle\/ ."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106284"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04652-0_5"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738007"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254098"},{"key":"e_1_2_2_30_1","volume-title":"Advanced Topics in Types and Programming Languages","author":"Pierce Benjamin C.","unstructured":"Benjamin C. Pierce . 2004. Advanced Topics in Types and Programming Languages . The MIT Press . Benjamin C. Pierce. 2004. Advanced Topics in Types and Programming Languages. The MIT Press."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_2_2_32_1","volume-title":"Lattice Theoretic Properties of Subsumption","author":"Plotkin Gordon","unstructured":"Gordon Plotkin . 1970. Lattice Theoretic Properties of Subsumption . Edinburgh University , Department of Machine Intelligence and Perception. https:\/\/books.google.com\/books?id=2p09cgAACAAJ Gordon Plotkin. 1970. Lattice Theoretic Properties of Subsumption. Edinburgh University, Department of Machine Intelligence and Perception. https:\/\/books.google.com\/books?id=2p09cgAACAAJ"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594321"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796817000016"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290386"},{"key":"e_1_2_2_37_1","volume-title":"Siek and Walid Taha","author":"Jeremy","year":"2006","unstructured":"Jeremy G. Siek and Walid Taha . 2006 . Gradual Typing for Functional Languages. In IN SCHEME AND FUNCTIONAL PROGRAMMING WORKSHOP . 81\u201392. Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In IN SCHEME AND FUNCTIONAL PROGRAMMING WORKSHOP . 81\u201392."},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706337"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-62688-3_47"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75283"},{"key":"e_1_2_2_42_1","volume-title":"POPL","author":"Wang Xinyu","year":"2018","unstructured":"Xinyu Wang , Isil Dillig , and Rishabh Singh . 2018. Program synthesis using abstraction refinement. PACMPL 2 , POPL ( 2018 ). Xinyu Wang, Isil Dillig, and Rishabh Singh. 2018. Program synthesis using abstraction refinement. PACMPL 2, POPL (2018)."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371080","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371080","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371080","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:42Z","timestamp":1750273542000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371080"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":41,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371080"],"URL":"https:\/\/doi.org\/10.1145\/3371080","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}