{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:10:00Z","timestamp":1784196600064,"version":"3.55.0"},"reference-count":110,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T00:00:00Z","timestamp":1749772800000},"content-version":"vor","delay-in-days":3,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["175281,2129008,2033558"],"award-info":[{"award-number":["175281,2129008,2033558"]}],"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":[[2025,6,10]]},"abstract":"<jats:p>\n                    When a program synthesis task starts from an ambiguous specification, the synthesis process often involves an iterative specification refinement process. We introduce the Programming by Navigation Synthesis Problem, a new synthesis problem adapted specifically for supporting iterative specification refinement in order to find a\n                    <jats:italic toggle=\"yes\">particular<\/jats:italic>\n                    target solution. In contrast to prior work, we prove that synthesizers that solve the Programming by Navigation Synthesis Problem show all valid next steps (\n                    <jats:bold>\n                      <jats:sc>Strong<\/jats:sc>\n                      <jats:sc>Completeness<\/jats:sc>\n                    <\/jats:bold>\n                    ) and only valid next steps (\n                    <jats:bold>\n                      <jats:sc>Strong<\/jats:sc>\n                      <jats:sc>Soundness<\/jats:sc>\n                    <\/jats:bold>\n                    ). To meet the demands of the Programming by Navigation Synthesis Problem, we introduce an algorithm to turn a type inhabitation oracle (in the style of classical logic) into a fully constructive program synthesizer.We then define such an oracle via sound compilation to Datalog. Our empirical evaluation shows that this technique results in an efficient Programming by Navigation synthesizer that solves tasks that are either impossible or too large for baselines to solve. Our synthesizer is the first to guarantee that its specification refinement process satisfies both\n                    <jats:bold>\n                      <jats:sc>Strong<\/jats:sc>\n                      <jats:sc>Completeness<\/jats:sc>\n                    <\/jats:bold>\n                    and\n                    <jats:bold>\n                      <jats:sc>Strong<\/jats:sc>\n                      <jats:sc>Soundness<\/jats:sc>\n                    <\/jats:bold>\n                    .\n                  <\/jats:p>","DOI":"10.1145\/3729264","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"447-474","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Programming by Navigation"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2311-1873","authenticated-orcid":false,"given":"Justin","family":"Lubin","sequence":"first","affiliation":[{"name":"University of California, Berkeley, Berkeley, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9462-2123","authenticated-orcid":false,"given":"Parker","family":"Ziegler","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, Berkeley, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0557-3580","authenticated-orcid":false,"given":"Sarah E.","family":"Chasins","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, Berkeley, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","unstructured":"Maaz Bin Safeer Ahmad and Alvin Cheung. 2018. Automatically Leveraging MapReduce Frameworks for Data- Intensive Applications. In Proceedings of the 2018 International Conference on Management of Data (SIGMOD). doi:10.1145\/3183713.3196891","DOI":"10.1145\/3183713.3196891"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","unstructured":"Maaz Bin Safeer Ahmad Jonathan Ragan-Kelley Alvin Cheung and Shoaib Kamil. 2019. Automatically Translating Image Processing Libraries to Halide. In ACM Transactions on Graphics (TOG). doi:10.1145\/3355089.3356549","DOI":"10.1145\/3355089.3356549"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","unstructured":"Aws Albarghouthi Sumit Gulwani and Zachary Kincaid. 2013. Recursive Program Synthesis. In Proceedings of the 25th International Conference on Computer Aided Verification (CAV). doi:10.1007\/978-3-642-39799-8_67","DOI":"10.1007\/978-3-642-39799-8_67"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","unstructured":"Aws Albarghouthi Paraschos Koutris Mayur Naik and Calvin Smith. 2017. Constraint-Based Synthesis of Datalog Programs. In Principles and Practice of Constraint Programming. doi:10.1007\/978-3-319-66158-2_44","DOI":"10.1007\/978-3-319-66158-2_44"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","unstructured":"Felicity Allen Fiona Behan Anton Khodak Francesco Iorio Kosuke Yusa Mathew Garnett and Leopold Parts. 2019. JACKS: Joint Analysis of CRISPR\/Cas9 Knockout Screens. In Genome Research. doi:10.1101\/gr.238923.118","DOI":"10.1101\/gr.238923.118"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","unstructured":"Dana Angluin. 1987. Learning Regular Sets from Queries and Counterexamples. In Information and Computation. doi:10.1016\/0890-5401(87)90052-6","DOI":"10.1016\/0890-5401(87)90052-6"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371090"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","unstructured":"Michael Arntzenius and Neelakantan R. Krishnaswami. 2016. Datafun: A Functional Datalog. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP). doi:10.1145\/2951913.2951948","DOI":"10.1145\/2951913.2951948"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","unstructured":"Francois Bancilhon David Maier Yehoshua Sagiv and Jeffrey D. Ullman. 1986. Magic Sets and Other Strange Ways to Implement Logic Programs (Extended Abstract). In Proceedings of the 5th ACM SIGACT-SIGMOD Symposium on Principles of Database Systems (PODS). doi:10.1145\/6012.15399","DOI":"10.1145\/6012.15399"},{"key":"e_1_3_2_11_2","unstructured":"Osbert Bastani Xin Zhang and Armando Solar-Lezama. 2021. Synthesizing Queries via Interactive Sketching. arXiv:1912.12659 https:\/\/arxiv.org\/abs\/1912.1265 [cs]"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3360594"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428209"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3689754"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","unstructured":"Sahil Bhatia Sumer Kohli Sanjit A. Seshia and Alvin Cheung. 2023. Building Code Transpilers for Domain-Specific Languages Using Program Synthesis. In 37th European Conference on Object-Oriented Programming (ECOOP). doi:10.4230\/LIPIcs.ECOOP.2023.38","DOI":"10.4230\/LIPIcs.ECOOP.2023.38"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","unstructured":"Andrew Blinn David Moon Eric Griffis and Cyrus Omar. 2022. An Integrative Human-Centered Architecture for Interactive Programming Assistants. In IEEE Symposium on Visual Languages and Human-Centric Computing (VL\/HCC). doi:10.1109\/VL\/HCC53370.2022.9833110","DOI":"10.1109\/VL\/HCC53370.2022.9833110"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","unstructured":"Christoph Bock Paul Datlinger Florence Chardon Matthew A. Coelho Matthew B. Dong Keith A. Lawson Tian Lu Laetitia Maroc Thomas M. Norman Bicna Song Geoff Stanley Sidi Chen Mathew Garnett Wei Li Jason Moffat Lei S. Qi Rebecca S. Shapiro Jay Shendure Jonathan S. Weissman and Xiaowei Zhuang. 2022. High-Content CRISPR Screening. In Nature Reviews Methods Primers. doi:10.1038\/s43586-021-00093-4","DOI":"10.1038\/s43586-021-00093-4"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","unstructured":"Sunil Bodapati Timothy P. Daley Xueqiu Lin James Zou and Lei S. Qi. 2020. A Benchmark of Algorithms for the Analysis of Pooled CRISPR Screens. In Genome Biology. doi:10.1186\/s13059-020-01972-x","DOI":"10.1186\/s13059-020-01972-x"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","unstructured":"Henrique Botelho Guerra Jo\u00e3o F. Ferreira and Jo\u00e3o Costa Seco. 2023. Hoogle\u2605: Constants and \u03bb-Abstractions in Petri-net-based Synthesis Using Symbolic Execution. In 37th European Conference on Object-Oriented Programming (ECOOP). doi:10.4230\/LIPIcs.ECOOP.2023.4","DOI":"10.4230\/LIPIcs.ECOOP.2023.4"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","unstructured":"Martin Bravenboer and Yannis Smaragdakis. 2009. Strictly Declarative Specification of Sophisticated Points-to Analyses. In Proceedings of the 24th ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA). doi:10.1145\/1640089.1640108","DOI":"10.1145\/1640089.1640108"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","unstructured":"Nicolas L. Bray Harold Pimentel P\u00e1ll Melsted and Lior Pachter. 2016. Near-Optimal Probabilistic RNA-seq Quantification. In Nature Biotechnology. doi:10.1038\/nbt.3519","DOI":"10.1038\/nbt.3519"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","unstructured":"Yanju Chen Chenglong Wang Xinyu Wang Osbert Bastani and Yu Feng. 2023. Fast and Reliable Program Synthesis via User Interaction. In 38th IEEE\/ACM International Conference on Automated Software Engineering (ASE). doi:10.1109\/ASE56229.2023.00129","DOI":"10.1109\/ASE56229.2023.00129"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","unstructured":"Alvin Cheung Armando Solar-Lezama and Samuel Madden. 2013. Optimizing Database-Backed Applications with Query Synthesis. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). doi:10.1145\/2491956.2462180","DOI":"10.1145\/2491956.2462180"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","unstructured":"Richard H. Connelly and F. Lockwood Morris. 1995. A Generalization of the Trie Data Structure. In Mathematical Structures in Computer Science. doi:10.1017\/S0960129500000803","DOI":"10.1017\/S0960129500000803"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","unstructured":"Matthew Conway Steve Audia Tommy Burnette Dennis Cosgrove and Kevin Christiansen. 2000. Alice: Lessons Learned from Building a 3D System for Novices. In Proceedings of the SIGCHI Conference on Human Factors in Computing Systems (CHI). doi:10.1145\/332040.332481","DOI":"10.1145\/332040.332481"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","unstructured":"Timothy P. Daley Zhixiang Lin Xueqiu Lin Yanxia Liu Wing Hung Wong and Lei S. Qi. 2018. CRISPhieRmix: A Hierarchical Mixture Model for CRISPR Pooled Screens. In Genome Biology. doi:10.1186\/s13059-018-1538-6","DOI":"10.1186\/s13059-018-1538-6"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","unstructured":"Aaron A. Diaz Han Qin Miguel Ramalho-Santos and Jun S. Song. 2015. HiTSelect: A Comprehensive Tool for High-Complexity-Pooled Screen Analysis. In Nucleic Acids Research. doi:10.1093\/nar\/gku1197","DOI":"10.1093\/nar\/gku1197"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","unstructured":"Alexander Dobin Carrie A. Davis Felix Schlesinger Jorg Drenkow Chris Zaleski Sonali Jha Philippe Batut Mark Chaisson and Thomas R. Gingeras. 2013. STAR: Ultrafast Universal RNA-seq Aligner. In Bioinformatics. doi:10.1093\/bioinformatics\/bts635","DOI":"10.1093\/bioinformatics\/bts635"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","unstructured":"Azadeh Farzan Danya Lette and Victor Nicolet. 2022. Recursion Synthesis with Unrealizability Witnesses. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI). doi:10.1145\/3519939.3523726","DOI":"10.1145\/3519939.3523726"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","unstructured":"Azadeh Farzan and Victor Nicolet. 2021. Counterexample-Guided Partial Bounding for Recursive Function Synthesis. In Computer Aided Verification (CAV). doi:10.1007\/978-3-030-81685-8_39","DOI":"10.1007\/978-3-030-81685-8_39"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","unstructured":"Yu Feng Ruben Martins Osbert Bastani and Isil Dillig. 2018. Program Synthesis Using Conflict-Driven Learning. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). doi:10.1145\/3192366.3192382","DOI":"10.1145\/3192366.3192382"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","unstructured":"Yu Feng Ruben Martins Jacob Van Geffen Isil Dillig and Swarat Chaudhuri. 2017. Component-Based Synthesis of Table Consolidation and Transformation Tasks from Examples. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). doi:10.1145\/3062341.3062351","DOI":"10.1145\/3062341.3062351"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","unstructured":"Yu Feng Ruben Martins Yuepeng Wang Isil Dillig and Thomas W. Reps. 2017. Component-Based Synthesis for Complex APIs. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). doi:10.1145\/27E9837.27E9851","DOI":"10.1145\/27E9837.27E9851"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","unstructured":"Yu Feng Xinyu Wang Isil Dillig and Thomas Dillig. 2015. Bottom-Up Context-Sensitive Pointer Analysis for Java. In Programming Languages and Systems (APLAS). doi:10.1007\/978-3-319-26529-2_25","DOI":"10.1007\/978-3-319-26529-2_25"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","unstructured":"John K. Feser Swarat Chaudhuri and Isil Dillig. 2015. Synthesizing Data Structure Transformations from Input-Output Examples. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). doi:10.1145\/2737924.2737977","DOI":"10.1145\/2737924.2737977"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","unstructured":"David B. Garlan and Philip L. Miller. 1984. GNOME: An Introductory Programming Environment Based on a Family of Structure Editors. In ACM SIGPLAN Notices. doi:10.1145\/390011.808250","DOI":"10.1145\/390011.808250"},{"key":"e_1_3_2_37_2","unstructured":"Gerhard Gentzen. 1964. Investigations into Logical Deduction. In American Philosophical Quarterly. jstor:20009142 https:\/\/www.jstor.org\/stable\/20009142"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","unstructured":"Sumit Gulwani. 2011. Automating String Processing in Spreadsheets Using Input-Output Examples. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). doi:10.1145\/1926385.1926423","DOI":"10.1145\/1926385.1926423"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","unstructured":"Sumit Gulwani Oleksandr Polozov and Rishabh Singh. 2017. Program Synthesis. doi:10.1561\/2500000010","DOI":"10.1561\/2500000010"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371080"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","unstructured":"Traver Hart and Jason Moffat. 2016. BAGEL: A Computational Framework for Identifying Essential Genes from Pooled Library Screens. In BMC Bioinformatics. doi:10.1186\/s12859-016-1015-8","DOI":"10.1186\/s12859-016-1015-8"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","unstructured":"Brian Hempel Justin Lubin Grace Lu and Ravi Chugh. 2018. Deuce: A Lightweight User Interface for Structured Editing. In Proceedings of the 40th International Conference on Software Engineering (ICSE). doi:10.1145\/3180155.3180165","DOI":"10.1145\/3180155.3180165"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","unstructured":"Martin Hofmann and Emanuel Kitzelmann. 2010. I\/O Guided Detection of List Catamorphisms: Towards Problem Specific Use of Program Templates in IP. In Proceedings of the 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM). doi:10.1145\/1706356.1706375","DOI":"10.1145\/1706356.1706375"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656381"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","unstructured":"Jingmei Hu Priyan Vaithilingam Stephen Chong Margo Seltzer and Elena L. Glassman. 2021. Assuage: Assembly Synthesis Using A Guided Exploration. In The 34th Annual ACM Symposium on User Interface Software and Technology (UIST). doi:10.1145\/3472749.3474740","DOI":"10.1145\/3472749.3474740"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428273"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","unstructured":"Susmit Jha Sumit Gulwani Sanjit A. Seshia and Ashish Tiwari. 2010. Oracle-Guided Component-Based Program Synthesis. In ACM\/IEEE 32nd International Conference on Software Engineering (ICSE). doi:10.1145\/1806799.1806833","DOI":"10.1145\/1806799.1806833"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","unstructured":"Ruyi Ji Jingjing Liang Yingfei Xiong Lu Zhang and Zhenjiang Hu. 2020. Question Selection for Interactive Program Synthesis. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). doi:10.1145\/3385412.3386025","DOI":"10.1145\/3385412.3386025"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","unstructured":"Shoaib Kamil Alvin Cheung Shachar Itzhaky and Armando Solar-Lezama. 2016. Verified Lifting of Stencil Computations. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). doi:10.1145\/2908080.2908117","DOI":"10.1145\/2908080.2908117"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","unstructured":"Etienne Kneuss Ivan Kuraj Viktor Kuncak and Philippe Suter. 2013. Synthesis Modulo Recursive Functions. In Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications (OOPSLA). doi:10.1145\/2509136.2509555","DOI":"10.1145\/2509136.2509555"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","unstructured":"Tristan Knoth Di Wang Nadia Polikarpova and Jan Hoffmann. 2019. Resource-Guided Program Synthesis. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). doi:10.1145\/3314221.3314602","DOI":"10.1145\/3314221.3314602"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","unstructured":"Amy J. Ko and Brad A. Myers. 2006. Barista: An Implementation Framework for Enabling New Tools Interaction Techniques and Views in Code Editors. In Proceedings of the SIGCHI Conference on Human Factors in Computing Systems (CHI). doi:10.1145\/1124772.1124831","DOI":"10.1145\/1124772.1124831"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","unstructured":"Renate K\u00f6nig Chih-yuan Chiang Buu P. Tu S. Frank Yan Paul D. DeJesus Angelica Romero Tobias Bergauer Anthony Orth Ute Krueger Yingyao Zhou and Sumit K. Chanda. 2007. A Probability-Based Approach for the Analysis of Large-Scale RNAi Screens. In Nature Methods. doi:10.1038\/nmeth1089","DOI":"10.1038\/nmeth1089"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/3547622"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","unstructured":"Ben Langmead and Steven L. Salzberg. 2012. Fast Gapped-Read Alignment with Bowtie 2. In Nature Methods. doi:10.1038\/nmeth.1923","DOI":"10.1038\/nmeth.1923"},{"key":"e_1_3_2_56_2","unstructured":"Vu Le Daniel Perelman Oleksandr Polozov Mohammad Raza Abhishek Udupa and Sumit Gulwani. 2017. Interactive Program Synthesis. arXiv:1703.03539 https:\/\/arxiv.org\/abs\/1703.03539 [cs]"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571263"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","unstructured":"Wei Li Johannes K\u00f6ster Han Xu Chen-Hao Chen Tengfei Xiao Jun S. Liu Myles Brown and X. Shirley Liu. 2015. Quality Control Modeling and Visualization of CRISPR Screens with MAGeCK-VISPR. In Genome Biology. doi:10.1186\/s13059-015-0843-6","DOI":"10.1186\/s13059-015-0843-6"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","unstructured":"Wei Li Han Xu Tengfei Xiao Le Cong Michael I. Love Feng Zhang Rafael A. Irizarry Jun S. Liu Myles Brown and X. Shirley Liu. 2014. MAGeCK Enables Robust Identification of Essential Genes from Genome-Scale CRISPR\/Cas9 Knockout Screens. In Genome Biology. doi:10.1186\/s13059-014-0554-4","DOI":"10.1186\/s13059-014-0554-4"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","unstructured":"Yang Liao Gordon K. Smyth and Wei Shi. 2014. featureCounts: An Efficient General Purpose Program for Assigning Sequence Reads to Genomic Features. In Bioinformatics. doi:10.1093\/bioinformatics\/btt656","DOI":"10.1093\/bioinformatics\/btt656"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","unstructured":"M. H. L\u00f6b. 1976. Embedding First Order Predicate Logic in Fragments of Intuitionistic Logic. In The Journal of Symbolic Logic. doi:10.2307\/2272390","DOI":"10.2307\/2272390"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","unstructured":"Michael I. Love Wolfgang Huber and Simon Anders. 2014. Moderated Estimation of Fold Change and Dispersion for RNA-seq Data with DESeq2. In Genome Biology. doi:10.1186\/s13059-014-0550-8","DOI":"10.1186\/s13059-014-0550-8"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1145\/3408991"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656453"},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","unstructured":"Justin Lubin Parker Ziegler and Sarah E. Chasins. 2025. Honeybee Docker Image. Zenodo. doi:10.5281\/zenodo.15033531","DOI":"10.5281\/zenodo.15033531"},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","unstructured":"Justin Lubin Parker Ziegler and Sarah E. Chasins. 2025. Honeybee Docker Image (Exact Version for Artifact Evaluation). Zenodo. doi:10.5281\/zenodo.15047790","DOI":"10.5281\/zenodo.15047790"},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","unstructured":"Magnus Madsen Ming-Ho Yee and Ond\u0159ej Lhot\u00e1k. 2016. From Datalog to Flix: A Declarative Language for Fixed Points on Lattices. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). doi:10.1145\/2908080.2908096","DOI":"10.1145\/2908080.2908096"},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","unstructured":"David Mandelin Lin Xu Rastislav Bod\u00edk 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). doi:10.1145\/1065010.1065018","DOI":"10.1145\/1065010.1065018"},{"key":"e_1_3_2_69_2","doi-asserted-by":"publisher","DOI":"10.1145\/3527315"},{"key":"e_1_3_2_70_2","doi-asserted-by":"publisher","unstructured":"Jeffrey G. Masek Michael A. Wulder Brian Markham Joel McCorkel Christopher J. Crawford James Storey and Del T. Jenstrom. 2020. Landsat 9: Empowering open science and applications through continuity. In Remote Sensing of Environment. doi:10.1016\/j.rse.2020.111968","DOI":"10.1016\/j.rse.2020.111968"},{"key":"e_1_3_2_71_2","doi-asserted-by":"publisher","unstructured":"Mika\u00ebl Mayer Gustavo Soares Maxim Grechkin Vu Le Mark Marron Oleksandr Polozov Rishabh Singh Benjamin Zorn and Sumit Gulwani. 2015. User Interaction Models for Disambiguation in Programming by Example. In Proceedings of the 28th Annual ACM Symposium on User Interface Software & Technology (UIST). doi:10.1145\/2807442.2807459","DOI":"10.1145\/2807442.2807459"},{"key":"e_1_3_2_72_2","doi-asserted-by":"publisher","unstructured":"Robin M. Meyers Jordan G. Bryan James M. McFarland Barbara A. Weir Ann E. Sizemore Han Xu Neekesh V. Dharia Phillip G. Montgomery Glenn S. Cowley Sasha Pantel Amy Goodale Yenarae Lee Levi D. Ali Guozhi Jiang Rakela Lubonja William F. Harrington Matthew Strickland Ting Wu Derek C. Hawes Victor A. Zhivich Meghan R. Wyatt Zohra Kalani Jaime J. Chang Michael Okamoto Kimberly Stegmaier Todd R. Golub Jesse S. Boehm Francisca Vazquez David E. Root William C. Hahn and Aviad Tsherniak. 2017. Computational Correction of Copy Number Effect Improves Specificity of CRISPR\u2013Cas9 Essentiality Screens in Cancer Cells. In Nature Genetics. doi:10.1038\/ng.3984","DOI":"10.1038\/ng.3984"},{"key":"e_1_3_2_73_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498682"},{"key":"e_1_3_2_74_2","doi-asserted-by":"publisher","unstructured":"Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 Theorem Prover and Programming Language. In Automated Deduction (CADE). doi:10.1007\/978-3-030-79876-5_37","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"e_1_3_2_75_2","doi-asserted-by":"publisher","unstructured":"Niek Mulleners Johan Jeuring and Bastiaan Heeren. 2023. Program Synthesis Using Example Propagation. In Practical Aspects of Declarative Languages (PADL). doi:10.1007\/978-3-031-24841-2_2","DOI":"10.1007\/978-3-031-24841-2_2"},{"key":"e_1_3_2_76_2","doi-asserted-by":"publisher","unstructured":"Daye Nam Baishakhi Ray Seohyun Kim Xianshan Qu and Satish Chandra. 2022. Predictive Synthesis of APIcentric Code. In Proceedings of the 6th ACM SIGPLAN International Symposium on Machine Programming (MAPS). doi:10.1145\/3520312.3534866","DOI":"10.1145\/3520312.3534866"},{"key":"e_1_3_2_77_2","unstructured":"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."},{"key":"e_1_3_2_78_2","doi-asserted-by":"publisher","unstructured":"Vegard Nygaard Einar Andreas R\u00f8dland and Eivind Hovig. 2016. Methods That Remove Batch Effects While Retaining Group Differences May Lead to Exaggerated Confidence in Downstream Analyses. In Biostatistics. doi:10.1093\/biostatistics\/kxv027","DOI":"10.1093\/biostatistics\/kxv027"},{"key":"e_1_3_2_79_2","doi-asserted-by":"publisher","unstructured":"Cyrus Omar Ian Voysey Michael Hilton Jonathan Aldrich and Matthew A. Hammer. 2017. Hazelnut: A Bidirectionally Typed Structure Editor Calculus. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). doi:10.1145\/27E9837.27E9900","DOI":"10.1145\/27E9837.27E9900"},{"key":"e_1_3_2_80_2","doi-asserted-by":"publisher","unstructured":"Peter-Michael Osera and Steve Zdancewic. 2015. Type-and-Example-Directed Program Synthesis. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). doi:10.1145\/2737924.2738007","DOI":"10.1145\/2737924.2738007"},{"key":"e_1_3_2_81_2","doi-asserted-by":"publisher","DOI":"10.1145\/3276520"},{"key":"e_1_3_2_82_2","doi-asserted-by":"publisher","unstructured":"Rob Patro Geet Duggal Michael I. Love Rafael A. Irizarry and Carl Kingsford. 2017. Salmon Provides Fast and Bias-Aware Quantification of Transcript Expression. In Nature Methods. doi:10.1038\/nmeth.4197","DOI":"10.1038\/nmeth.4197"},{"key":"e_1_3_2_83_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428227"},{"key":"e_1_3_2_84_2","doi-asserted-by":"publisher","unstructured":"Hila Peleg Shachar Itzhaky and Sharon Shoham. 2018. Abstraction-Based Interaction Model for Synthesis. In Verification Model Checking and Abstract Interpretation (VMCAI). doi:10.1007\/978-3-319-73721-8_18","DOI":"10.1007\/978-3-319-73721-8_18"},{"key":"e_1_3_2_85_2","doi-asserted-by":"publisher","unstructured":"Hila Peleg Sharon Shoham and Eran Yahav. 2018. Programming Not Only by Example. In IEEE\/ACM 40th International Conference on Software Engineering (ICSE). doi:10.1145\/3180155.3180189","DOI":"10.1145\/3180155.3180189"},{"key":"e_1_3_2_86_2","doi-asserted-by":"publisher","unstructured":"Nadia Polikarpova Ivan Kuraj and Armando Solar-Lezama. 2016. Program Synthesis from Polymorphic Refinement Types. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). doi:10.1145\/2908080.2908093","DOI":"10.1145\/2908080.2908093"},{"key":"e_1_3_2_87_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371130"},{"key":"e_1_3_2_88_2","doi-asserted-by":"publisher","unstructured":"Mitchel Resnick John Maloney Andr\u00e9s Monroy-Hern\u00e1ndez Natalie Rusk Evelyn Eastmond Karen Brennan Amon Millner Eric Rosenbaum Jay Silver Brian Silverman and Yasmin Kafai. 2009. Scratch: Programming for All. In Communications of the ACM (CACM). doi:10.1145\/1592761.1592779","DOI":"10.1145\/1592761.1592779"},{"key":"e_1_3_2_89_2","doi-asserted-by":"publisher","unstructured":"The Rocq Development Team. 2025. The Rocq Prover. Zenodo. doi:10.5281\/zenodo.15149629","DOI":"10.5281\/zenodo.15149629"},{"key":"e_1_3_2_90_2","volume-title":"Monitoring Vegetation Systems in the Great Plains with ERTS","author":"Rouse J. W.","year":"1974","unstructured":"J. W. Rouse, R. H. Haas, J. A. Schell, and D. W. Deering. 1974. Monitoring Vegetation Systems in the Great Plains with ERTS. Technical Report. NASA. https:\/\/ntrs.nasa.gov\/citations\/19740022614"},{"key":"e_1_3_2_91_2","doi-asserted-by":"publisher","unstructured":"Bernhard Scholz Herbert Jordan Pavle Subotic and Till Westmann. 2016. On Fast Large-Scale Program Analysis in Datalog. In Proceedings of the 25th International Conference on Compiler Construction (CC). doi:10.1145\/2892208.2892226","DOI":"10.1145\/2892208.2892226"},{"key":"e_1_3_2_92_2","doi-asserted-by":"publisher","unstructured":"Ophir Shalem Neville E. Sanjana Ella Hartenian Xi Shi David A. Scott Tarjei S. Mikkelsen Dirk Heckl Benjamin L. Ebert David E. Root John G. Doench and Feng Zhang. 2014. Genome-Scale CRISPR-Cas9 Knockout Screening in Human Cells. In Science. doi:10.1126\/science.1247005","DOI":"10.1126\/science.1247005"},{"key":"e_1_3_2_93_2","doi-asserted-by":"publisher","unstructured":"Kensen Shi David Bieber and Rishabh Singh. 2022. TF-Coder: Program Synthesis for Tensor Manipulations. In ACM Transactions on Programming Languages and Systems (TOPLAS). doi:10.1145\/3517034","DOI":"10.1145\/3517034"},{"key":"e_1_3_2_94_2","doi-asserted-by":"publisher","unstructured":"Xujie Si Woosuk Lee Richard Zhang Aws Albarghouthi Paraschos Koutris and Mayur Naik. 2018. Syntax-Guided Synthesis of Datalog Programs. In Proceedings of the 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC\/FSE). doi:10.1145\/3236024.3236034","DOI":"10.1145\/3236024.3236034"},{"key":"e_1_3_2_95_2","doi-asserted-by":"publisher","unstructured":"Calvin Smith and Aws Albarghouthi. 2016. MapReduce Program Synthesis. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). doi:10.1145\/2908080.2908102","DOI":"10.1145\/2908080.2908102"},{"key":"e_1_3_2_96_2","doi-asserted-by":"publisher","unstructured":"Armando Solar-Lezama Christopher Grant Jones and Rastislav Bodik. 2008. Sketching Concurrent Data Structures. In Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). doi:10.1145\/1375581.1375599","DOI":"10.1145\/1375581.1375599"},{"key":"e_1_3_2_97_2","doi-asserted-by":"publisher","unstructured":"Armando Solar-Lezama Liviu Tancau Rastislav Bodik Sanjit Seshia and Vijay Saraswat. 2006. Combinatorial Sketching for Finite Programs. In Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS). doi:10.1145\/1168857.1168907","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_2_98_2","doi-asserted-by":"publisher","unstructured":"Jerry Swan Krzysztof Krawiec and Zoltan A. Kocsis. 2019. Stochastic Synthesis of Recursive Functions Made Easy with Bananas Lenses Envelopes and Barbed Wire. In Genetic Programming and Evolvable Machines. doi:10.1007\/s10710-019-09347-3","DOI":"10.1007\/s10710-019-09347-3"},{"key":"e_1_3_2_99_2","doi-asserted-by":"publisher","DOI":"10.1145\/3276509"},{"key":"e_1_3_2_100_2","doi-asserted-by":"publisher","unstructured":"Tim Teitelbaum and Thomas Reps. 1981. The Cornell Program Synthesizer: A Syntax-Directed Programming Environment. In Communications of the ACM (CACM). doi:10.1145\/358746.358755","DOI":"10.1145\/358746.358755"},{"key":"e_1_3_2_101_2","doi-asserted-by":"publisher","unstructured":"Chenglong Wang Alvin Cheung and Rastislav Bodik. 2017. Interactive Query Synthesis from Input-Output Examples. In Proceedings of the 2017 ACM International Conference on Management of Data (SIGMOD). doi:10.1145\/3035918.3058738","DOI":"10.1145\/3035918.3058738"},{"key":"e_1_3_2_102_2","doi-asserted-by":"publisher","unstructured":"Tim Wang Jenny J. Wei David M. Sabatini and Eric S. Lander. 2014. Genetic Screens in Human Cells Using the CRISPR-Cas9 System. In Science. doi:10.1126\/science.1246981","DOI":"10.1126\/science.1246981"},{"key":"e_1_3_2_103_2","doi-asserted-by":"publisher","unstructured":"Yuepeng Wang Rushi Shah Abby Criswell Rong Pan and Isil Dillig. 2020. Data Migration Using Datalog Program Synthesis. In Proceedings of the VLDB Endowment. doi:10.14778\/3384345.3384350","DOI":"10.14778\/3384345.3384350"},{"key":"e_1_3_2_104_2","doi-asserted-by":"publisher","unstructured":"John Whaley Dzintars Avots Michael Carbin and Monica S. Lam. 2005. Using Datalog with Binary Decision Diagrams for Program Analysis. In Programming Languages and Systems (APLAS). doi:10.1007\/11575467_8","DOI":"10.1007\/11575467_8"},{"key":"e_1_3_2_105_2","doi-asserted-by":"publisher","unstructured":"A. K. Wright and M. Felleisen. 1994. A Syntactic Approach to Type Soundness. In Information and Computation. doi:10.1006\/inco.1994.1093","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_3_2_106_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591255"},{"key":"e_1_3_2_107_2","doi-asserted-by":"publisher","unstructured":"Tianyi Zhang Zhiyang Chen Yuanli Zhu Priyan Vaithilingam Xinyu Wang and Elena L. Glassman. 2021. Interpretable Program Synthesis. In Proceedings of the 2021 CHI Conference on Human Factors in Computing Systems (CHI). doi:10.1145\/3411764.3445646","DOI":"10.1145\/3411764.3445646"},{"key":"e_1_3_2_108_2","doi-asserted-by":"publisher","unstructured":"Tianyi Zhang London Lowmanstone Xinyu Wang and Elena L. Glassman. 2020. Interactive Program Synthesis by Augmented Examples. In Proceedings of the 33rd Annual ACM Symposium on User Interface Software and Technology (UIST). doi:10.1145\/3379337.3415900","DOI":"10.1145\/3379337.3415900"},{"key":"e_1_3_2_109_2","doi-asserted-by":"publisher","unstructured":"Yuqing Zhang Giovanni Parmigiani and W. Evan Johnson. 2020. ComBat-seq: Batch Effect Adjustment for RNA-seq Count Data. In NAR Genomics and Bioinformatics. doi:10.1093\/nargab\/lqaa078","DOI":"10.1093\/nargab\/lqaa078"},{"key":"e_1_3_2_110_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591239"},{"key":"e_1_3_2_111_2","doi-asserted-by":"publisher","unstructured":"Zhanhui Zhou Man To Tang Qiping Pan Shangyin Tan Xinyu Wang and Tianyi Zhang. 2022. INTENT: Interactive Tensor Transformation Synthesis. In Proceedings of the 35th Annual ACM Symposium on User Interface Software and Technology (UIST). doi:10.1145\/3526113.3545653","DOI":"10.1145\/3526113.3545653"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729264","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729264","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:01:03Z","timestamp":1784196063000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729264"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":110,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729264"],"URL":"https:\/\/doi.org\/10.1145\/3729264","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}