{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,24]],"date-time":"2026-06-24T08:22:12Z","timestamp":1782289332725,"version":"3.54.5"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2020,8,2]],"date-time":"2020-08-02T00:00:00Z","timestamp":1596326400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"National Science Foundation","award":["1814900, 1817145, 1651794"],"award-info":[{"award-number":["1814900, 1817145, 1651794"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,8,2]]},"abstract":"<jats:p>We present a system called Smyth for program sketching in a typed functional language whereby the concrete evaluation of ordinary assertions gives rise to input-output examples, which are then used to guide the search to complete the holes. The key innovation, called live bidirectional evaluation, propagates examples \"backward\" through partially evaluated sketches. Live bidirectional evaluation enables Smyth to (a) synthesize recursive functions without trace-complete sets of examples and (b) specify and solve interdependent synthesis goals. Eliminating the trace-completeness requirement resolves a significant limitation faced by prior synthesis techniques when given partial specifications in the form of input-output examples.<\/jats:p>\n          <jats:p>To assess the practical implications of our techniques, we ran several experiments on benchmarks used to evaluate Myth, a state-of-the-art example-based synthesis tool. First, given expert examples (and no partial implementations), we find that Smyth requires on average 66% of the number of expert examples required by Myth. Second, we find that Smyth is robust to randomly-generated examples, synthesizing many tasks with relatively few more random examples than those provided by an expert. Third, we create a suite of small sketching tasks by systematically employing a simple sketching strategy to the Myth benchmarks; we find that user-provided sketches in Smyth often further reduce the total specification burden (i.e. the combination of partial implementations and examples). Lastly, we find that Leon and Synquid, two state-of-the-art logic-based synthesis tools, fail to complete several tasks on which Smyth succeeds.<\/jats:p>","DOI":"10.1145\/3408991","type":"journal-article","created":{"date-parts":[[2020,8,3]],"date-time":"2020-08-03T13:48:02Z","timestamp":1596462482000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":42,"title":["Program sketching with live bidirectional evaluation"],"prefix":"10.1145","volume":"4","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2311-1873","authenticated-orcid":false,"given":"Justin","family":"Lubin","sequence":"first","affiliation":[{"name":"University of Chicago, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6578-2005","authenticated-orcid":false,"given":"Nick","family":"Collins","sequence":"additional","affiliation":[{"name":"University of Chicago, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4502-7971","authenticated-orcid":false,"given":"Cyrus","family":"Omar","sequence":"additional","affiliation":[{"name":"University of Michigan, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1339-2889","authenticated-orcid":false,"given":"Ravi","family":"Chugh","sequence":"additional","affiliation":[{"name":"University of Chicago, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2020,8,3]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"crossref","unstructured":"Aws Albarghouthi Sumit Gulwani and Zachary Kincaid. 2013. Recursive Program Synthesis. In Computer Aided Verification (CAV).  Aws Albarghouthi Sumit Gulwani and Zachary Kincaid. 2013. Recursive Program Synthesis. In Computer Aided Verification (CAV).","DOI":"10.1007\/978-3-642-39799-8_67"},{"key":"e_1_2_2_2_1","doi-asserted-by":"crossref","unstructured":"Rajeev Alur Rastislav Bodik Garvit Juniwal Milo M. K. Martin Mukund Raghothaman Sanjit A. Seshia Rishabh Singh Armando Solar-Lezama Emina Torlak and Abhishek Udupa. 2013. Syntax-Guided Synthesis. In Formal Methods in Computer-Aided Design (FMCAD).  Rajeev Alur Rastislav Bodik Garvit Juniwal Milo M. K. Martin Mukund Raghothaman Sanjit A. Seshia Rishabh Singh Armando Solar-Lezama Emina Torlak and Abhishek Udupa. 2013. Syntax-Guided Synthesis. In Formal Methods in Computer-Aided Design (FMCAD).","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_2_2_3_1","volume-title":"The Logic of Relevance and Necessity","author":"Anderson Alan Ross","unstructured":"Alan Ross Anderson , Nuel D. Belnap Jr ., and J. Michael Dunn . 1992. Entailment , Vol. II : The Logic of Relevance and Necessity . Princeton University Press . Alan Ross Anderson, Nuel D. Belnap Jr., and J. Michael Dunn. 1992. Entailment, Vol. II: The Logic of Relevance and Necessity. Princeton University Press."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276519"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3242587.3242661"},{"key":"e_1_2_2_7_1","volume-title":"Strict Bidirectional Type Checking. In Workshop on Types in Languages Design and Implementation (TLDI).","author":"Chlipala Adam","year":"2005","unstructured":"Adam Chlipala , Leaf Petersen , and Robert Harper . 2005 . Strict Bidirectional Type Checking. In Workshop on Types in Languages Design and Implementation (TLDI). Adam Chlipala, Leaf Petersen, and Robert Harper. 2005. Strict Bidirectional Type Checking. In Workshop on Types in Languages Design and Implementation (TLDI)."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062351"},{"key":"e_1_2_2_9_1","volume-title":"Component-Based Synthesis for Complex APIs. In Symposium on Principles of Programming Languages (POPL).","author":"Feng Yu","unstructured":"Yu Feng , Ruben Martins , Yuepeng Wang , Isil Dillig , and Thomas W. Reps . 2017b . Component-Based Synthesis for Complex APIs. In Symposium on Principles of Programming Languages (POPL). Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, and Thomas W. Reps. 2017b. Component-Based Synthesis for Complex APIs. In Symposium on Principles of Programming Languages (POPL)."},{"key":"e_1_2_2_10_1","volume-title":"Inductive Program Synthesis from Input-Output Examples. Master's Thesis","author":"Feser John","unstructured":"John Feser . 2016. Inductive Program Synthesis from Input-Output Examples. Master's Thesis , Rice University . John Feser. 2016. Inductive Program Synthesis from Input-Output Examples. Master's Thesis, Rice University."},{"key":"e_1_2_2_11_1","volume-title":"February","author":"Feser John","year":"2020","unstructured":"John Feser . 2020. Personal communication , February 2020 . John Feser. 2020. Personal communication, February 2020."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737977"},{"key":"e_1_2_2_13_1","volume-title":"Example-Directed Synthesis: A TypeTheoretic Interpretation. In Symposium on Principles of Programming Languages (POPL).","author":"Frankle Jonathan","year":"2016","unstructured":"Jonathan Frankle , Peter-Michael Osera , David Walker , and Steve Zdancewic . 2016 . Example-Directed Synthesis: A TypeTheoretic Interpretation. In Symposium on Principles of Programming Languages (POPL). Jonathan Frankle, Peter-Michael Osera, David Walker, and Steve Zdancewic. 2016. Example-Directed Synthesis: A TypeTheoretic Interpretation. In Symposium on Principles of Programming Languages (POPL)."},{"key":"e_1_2_2_14_1","volume-title":"Automating String Processing in Spreadsheets Using Input-Output Examples. In Symposium on Principles of Programming Languages (POPL).","author":"Gulwani Sumit","year":"2011","unstructured":"Sumit Gulwani . 2011 . Automating String Processing in Spreadsheets Using Input-Output Examples. In Symposium on Principles of Programming Languages (POPL). Sumit Gulwani. 2011. Automating String Processing in Spreadsheets Using Input-Output Examples. In Symposium on Principles of Programming Languages (POPL)."},{"key":"e_1_2_2_15_1","volume-title":"StriSynth: Synthesis for Live Programming. In International Conference on Software Engineering (ICSE).","author":"Gulwani Sumit","year":"2015","unstructured":"Sumit Gulwani , Mika\u00ebl Mayer , Filip Niksic , and Ruzica Piskac . 2015 . StriSynth: Synthesis for Live Programming. In International Conference on Software Engineering (ICSE). Sumit Gulwani, Mika\u00ebl Mayer, Filip Niksic, and Ruzica Piskac. 2015. StriSynth: Synthesis for Live Programming. In International Conference on Software Engineering (ICSE)."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000010"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371080"},{"key":"e_1_2_2_18_1","volume-title":"Complete Completion Using Types and Weights. In Conference on Programming Language Design and Implementation (PLDI).","author":"Gvero Tihomir","year":"2013","unstructured":"Tihomir Gvero , Viktor Kuncak , Ivan Kuraj , and Ruzica Piskac . 2013 . Complete Completion Using Types and Weights. In Conference on Programming Language Design and Implementation (PLDI). Tihomir Gvero, Viktor Kuncak, Ivan Kuraj, and Ruzica Piskac. 2013. Complete Completion Using Types and Weights. In Conference on Programming Language Design and Implementation (PLDI)."},{"key":"e_1_2_2_19_1","volume-title":"Output-Directed Programming for SVG. In Symposium on User Interface Software and Technology (UIST).","author":"Hempel Brian","year":"2019","unstructured":"Brian Hempel , Justin Lubin , and Ravi Chugh . 2019 . Output-Directed Programming for SVG. In Symposium on User Interface Software and Technology (UIST). Brian Hempel, Justin Lubin, and Ravi Chugh. 2019. Output-Directed Programming for SVG. In Symposium on User Interface Software and Technology (UIST)."},{"key":"e_1_2_2_20_1","unstructured":"Jeevana Priya Inala Nadia Polikarpova Xiaokang Qiu Benjamin S. Lerner and Armando Solar-Lezama. 2017. Synthesis of Recursive ADT Transformations from Reusable Templates. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS).  Jeevana Priya Inala Nadia Polikarpova Xiaokang Qiu Benjamin S. Lerner and Armando Solar-Lezama. 2017. Synthesis of Recursive ADT Transformations from Reusable Templates. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS)."},{"key":"e_1_2_2_21_1","volume-title":"Natural Semantics. In Symposium on Theoretical Aspects of Computer Sciences (STACS).","author":"Kahn Gilles","year":"1987","unstructured":"Gilles Kahn . 1987 . Natural Semantics. In Symposium on Theoretical Aspects of Computer Sciences (STACS). Gilles Kahn. 1987. Natural Semantics. In Symposium on Theoretical Aspects of Computer Sciences (STACS)."},{"key":"e_1_2_2_22_1","doi-asserted-by":"crossref","unstructured":"Etienne Kneuss Manos Koukoutos and Viktor Kuncak. 2015. Deductive Program Repair. In Computer Aided Verification (CAV).  Etienne Kneuss Manos Koukoutos and Viktor Kuncak. 2015. Deductive Program Repair. In Computer Aided Verification (CAV).","DOI":"10.1007\/978-3-319-21668-3_13"},{"key":"e_1_2_2_23_1","volume-title":"Synthesis Modulo Recursive Functions. In Conference on Object-Oriented Programming Languages, Systems, and Applications (OOPSLA).","author":"Kneuss Etienne","year":"2013","unstructured":"Etienne Kneuss , Ivan Kuraj , Viktor Kuncak , and Philippe Suter . 2013 . Synthesis Modulo Recursive Functions. In Conference on Object-Oriented Programming Languages, Systems, and Applications (OOPSLA). Etienne Kneuss, Ivan Kuraj, Viktor Kuncak, and Philippe Suter. 2013. Synthesis Modulo Recursive Functions. In Conference on Object-Oriented Programming Languages, Systems, and Applications (OOPSLA)."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180200"},{"key":"e_1_2_2_25_1","volume-title":"Program Sketching with Live Bidirectional Evaluation. Extended version of this ICFP 2020 paper available as CoRR abs\/","author":"Lubin Justin","year":"1911","unstructured":"Justin Lubin , Nick Collins , Cyrus Omar , and Ravi Chugh . 2020. Program Sketching with Live Bidirectional Evaluation. Extended version of this ICFP 2020 paper available as CoRR abs\/ 1911 .00583 (https:\/\/arxiv.org\/abs\/ 1911.00583). Justin Lubin, Nick Collins, Cyrus Omar, and Ravi Chugh. 2020. Program Sketching with Live Bidirectional Evaluation. Extended version of this ICFP 2020 paper available as CoRR abs\/ 1911.00583 (https:\/\/arxiv.org\/abs\/ 1911.00583)."},{"key":"e_1_2_2_26_1","volume-title":"HOBiT: Programming Lenses Without Using Lens Combinators. In European Symposium on Programming (ESOP).","author":"Matsuda Kazutaka","year":"2018","unstructured":"Kazutaka Matsuda and Meng Wang . 2018 . HOBiT: Programming Lenses Without Using Lens Combinators. In European Symposium on Programming (ESOP). Kazutaka Matsuda and Meng Wang. 2018. HOBiT: Programming Lenses Without Using Lens Combinators. In European Symposium on Programming (ESOP)."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276497"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341699"},{"key":"e_1_2_2_29_1","volume-title":"Data-Driven Inference of Representation Invariants. In Conference on Programming Language Design and Implementation (PLDI).","author":"Miltner Anders","year":"2020","unstructured":"Anders Miltner , Saswat Padhi , Todd D. Millstein , and David Walker . 2020 . Data-Driven Inference of Representation Invariants. In Conference on Programming Language Design and Implementation (PLDI). Anders Miltner, Saswat Padhi, Todd D. Millstein, and David Walker. 2020. Data-Driven Inference of Representation Invariants. In Conference on Programming Language Design and Implementation (PLDI)."},{"key":"e_1_2_2_30_1","doi-asserted-by":"crossref","unstructured":"Aleksandar Nanevski Frank Pfenning and Brigitte Pientka. 2008. Contextual Modal Type Theory. ACM Transactions on Computational Logic (TOCL) ( 2008 ).  Aleksandar Nanevski Frank Pfenning and Brigitte Pientka. 2008. Contextual Modal Type Theory. ACM Transactions on Computational Logic (TOCL) ( 2008 ).","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_2_2_31_1","volume-title":"Proceedings of the ACM on Programming Languages (PACMPL), Issue POPL ( 2019 ).","author":"Omar Cyrus","unstructured":"Cyrus Omar , Ian Voysey , Ravi Chugh , and Matthew A. Hammer . 2019. Live Functional Programming with Typed Holes . Proceedings of the ACM on Programming Languages (PACMPL), Issue POPL ( 2019 ). Cyrus Omar, Ian Voysey, Ravi Chugh, and Matthew A. Hammer. 2019. Live Functional Programming with Typed Holes. Proceedings of the ACM on Programming Languages (PACMPL), Issue POPL ( 2019 )."},{"key":"e_1_2_2_33_1","volume-title":"Type-and-Example-Directed Program Synthesis. In Conference on Programming Language Design and Implementation (PLDI).","author":"Osera Peter-Michael","year":"2015","unstructured":"Peter-Michael Osera and Steve Zdancewic . 2015 . Type-and-Example-Directed Program Synthesis. In Conference on Programming Language Design and Implementation (PLDI). Peter-Michael Osera and Steve Zdancewic. 2015. Type-and-Example-Directed Program Synthesis. In Conference on Programming Language Design and Implementation (PLDI)."},{"key":"e_1_2_2_34_1","volume-title":"Functional Programs That Explain Their Work. In International Conference on Functional Programming (ICFP).","author":"Perera Roly","year":"2012","unstructured":"Roly Perera , Umut A. Acar , James Cheney , and Paul Blain Levy . 2012 . Functional Programs That Explain Their Work. In International Conference on Functional Programming (ICFP). Roly Perera, Umut A. Acar, James Cheney, and Paul Blain Levy. 2012. Functional Programs That Explain Their Work. In International Conference on Functional Programming (ICFP)."},{"key":"e_1_2_2_35_1","volume-title":"Turner","author":"Pierce Benjamin C.","year":"2000","unstructured":"Benjamin C. Pierce and David N . Turner . 2000 . Local Type Inference. ACM Transactions on Programming Languages and Systems (TOPLAS) ( 2000 ). Benjamin C. Pierce and David N. Turner. 2000. Local Type Inference. ACM Transactions on Programming Languages and Systems (TOPLAS) ( 2000 )."},{"key":"e_1_2_2_36_1","volume-title":"Personal communication, February and May","author":"Polikarpova Nadia","year":"2020","unstructured":"Nadia Polikarpova . 2020. Personal communication, February and May 2020 . Nadia Polikarpova. 2020. Personal communication, February and May 2020."},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_2_2_38_1","volume-title":"Liquid Types. In Conference on Programming Language Design and Implementation (PLDI).","author":"Rondon Patrick M.","year":"2008","unstructured":"Patrick M. Rondon , Ming Kawaguci , and Ranjit Jhala . 2008 . Liquid Types. In Conference on Programming Language Design and Implementation (PLDI). Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala. 2008. Liquid Types. In Conference on Programming Language Design and Implementation (PLDI)."},{"key":"e_1_2_2_39_1","volume-title":"Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop.","author":"Jeremy","unstructured":"Jeremy G. Siek and Walid Taha. 2006 . Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop. Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop."},{"key":"e_1_2_2_40_1","unstructured":"Jeremy G. Siek Michael M. Vitousek Matteo Cimini and John Tang Boyland. 2015. Refined Criteria for Gradual Typing. In Summit on Advances in Programming Languages (SNAPL).  Jeremy G. Siek Michael M. Vitousek Matteo Cimini and John Tang Boyland. 2015. Refined Criteria for Gradual Typing. In Summit on Advances in Programming Languages (SNAPL)."},{"key":"e_1_2_2_41_1","volume-title":"MapReduce Program Synthesis. In Conference on Programming Language Design and Implementation (PLDI).","author":"Smith Calvin","year":"2016","unstructured":"Calvin Smith and Aws Albarghouthi . 2016 . MapReduce Program Synthesis. In Conference on Programming Language Design and Implementation (PLDI). Calvin Smith and Aws Albarghouthi. 2016. MapReduce Program Synthesis. In Conference on Programming Language Design and Implementation (PLDI)."},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_3"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065045"},{"key":"e_1_2_2_45_1","volume-title":"Combinatorial Sketching for Finite Programs. In International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS).","author":"Solar-Lezama Armando","year":"2006","unstructured":"Armando Solar-Lezama , Liviu Tancau , Rastislav Bodik , Sanjit Seshia , and Vijay Saraswat . 2006 . Combinatorial Sketching for Finite Programs. In International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS). Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit Seshia, and Vijay Saraswat. 2006. Combinatorial Sketching for Finite Programs. In International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)."},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/LIVE.2013.6617346"},{"key":"e_1_2_2_47_1","volume-title":"Growing Solver-Aided Languages with Rosette. In Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software (Onward!).","author":"Torlak Emina","year":"2013","unstructured":"Emina Torlak and Rastislav Bodik . 2013 . Growing Solver-Aided Languages with Rosette. In Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software (Onward!). Emina Torlak and Rastislav Bodik. 2013. Growing Solver-Aided Languages with Rosette. In Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software (Onward!)."},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594340"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_13"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371117"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3408991","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3408991","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3408991","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:59Z","timestamp":1750193279000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3408991"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,8,2]]},"references-count":47,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2020,8,2]]}},"alternative-id":["10.1145\/3408991"],"URL":"https:\/\/doi.org\/10.1145\/3408991","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,8,2]]},"assertion":[{"value":"2020-08-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}