{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:56Z","timestamp":1780994696900,"version":"3.54.1"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["2107206, 2145649"],"award-info":[{"award-number":["2107206, 2145649"]}],"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":[[2024,1,2]]},"abstract":"<jats:p>Random generation of well-typed terms lies at the core of effective random testing of compilers for functional languages. Existing techniques have had success following a top-down type-oriented approach to generation that makes choices locally, which suffers from an inherent limitation: the type of an expression is often generated independently from the expression itself. Such generation frequently yields functions with argument types that cannot be used to produce a result in a meaningful way, leaving those arguments unused. Such \u201cuse-less\u201d functions can hinder both performance, as the argument generation code is dead but still needs to be compiled, and effectiveness, as a lot of interesting optimizations are tested less frequently.<\/jats:p>\n                  <jats:p>In this paper, we introduce a novel algorithm that is significantly more effective at generating functions that use their arguments. We formalize both the \u201clocal\u201d and the \u201cnonlocal\u201d algorithms as step-relations in an extension of the simply-typed lambda calculus with type and arguments holes, showing how delaying the generation of types for subexpressions by allowing nonlocal generation steps leads to \u201cuseful\u201d functions. We implement our algorithm demonstrating that it\u2019s much closer to real programs in terms of argument usage rate, and we replicate a case study from the literature that finds bugs in the strictness analyzer of GHC, with our approach finding bugs four times faster than the current state-of-the-art local approach.<\/jats:p>","DOI":"10.1145\/3632919","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T15:48:51Z","timestamp":1704469731000},"page":"2318-2339","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Generating Well-Typed Terms That Are Not \u201cUseless\u201d"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-7024-7331","authenticated-orcid":false,"given":"Justine","family":"Frank","sequence":"first","affiliation":[{"name":"University of Maryland, College Park, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6922-9706","authenticated-orcid":false,"given":"Benjamin","family":"Quiring","sequence":"additional","affiliation":[{"name":"University of Maryland, College Park, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0269-9815","authenticated-orcid":false,"given":"Leonidas","family":"Lampropoulos","sequence":"additional","affiliation":[{"name":"University of Maryland, College Park, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94460-9_7"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-51676-9_8"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796815000143"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2019.04.002"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001535"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0963548304006315"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364506.2364515"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2013.6698888"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737977"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_16"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90226-7"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.8423782"},{"key":"e_1_3_1_14_1","author":"Goldstein Harrison","year":"2021","unstructured":"Harrison Goldstein, John Hughes, Leonidas Lampropoulos, and Benjamin C. Pierce. 2021. Do Judge a Test by its Cover: Combining Combinatorial and Property-Based Testing.","journal-title":"Do Judge a Test by its Cover: Combining Combinatorial and Property-Based Testing"},{"key":"e_1_3_1_15_1","article-title":"Counting and generating lambda terms","author":"Grygiel Katarzyna","year":"2012","unstructured":"Katarzyna Grygiel and Pierre Lescanne. 2012. Counting and generating lambda terms. CoRR abs\/1210.2610 (2012). arXiv:1210.2610 http:\/\/arxiv.org\/abs\/1210.2610","journal-title":"CoRR abs\/1210.2610"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1561\/9781680832938"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001891"},{"key":"e_1_3_1_18_1","article-title":"Random Testing of a Higher-Order Blockchain Language (Experience Report)","author":"Hoang Tram","year":"2022","unstructured":"Tram Hoang, Anton Trunov, Leonidas Lampropoulos, and Ilya Sergey. 2022. Random Testing of a Higher-Order Blockchain Language (Experience Report). In Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP).","journal-title":"Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP)"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/503502.503505"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000263"},{"key":"e_1_3_1_21_1","doi-asserted-by":"crossref","unstructured":"Leonidas Lampropoulos Diane Gallois-Wong Catalin Hritcu John Hughes Benjamin C. Pierce and Li-yao Xia. 2017a. Beginner\u2019s Luck: a language for property-based generators. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages POPL 2017 Paris France January 18-20 2017. 114\u2013129. http:\/\/dl.acm.org\/citation.cfm?id=3009868","DOI":"10.1145\/3009837.3009868"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122955.3122959"},{"key":"e_1_3_1_23_1","article-title":"Boltzmann samplers for random generation of lambda terms","author":"Lescanne Pierre","year":"2014","unstructured":"Pierre Lescanne. 2014. Boltzmann samplers for random generation of lambda terms. CoRR abs\/1404.3875 (2014). http:\/\/arxiv.org\/abs\/1404.3875","journal-title":"CoRR abs\/1404.3875"},{"key":"e_1_3_1_24_1","article-title":"A Formal Model of Checked C","author":"Li Liyi","year":"2022","unstructured":"Liyi Li, Yiyun Liu, Deena L. Postol, Leonidas Lampropoulos, David Van Horn, and Michael Hicks. 2022. A Formal Model of Checked C. In Proceedings of the Computer Security Foundations Symposium (CSF).","journal-title":"Proceedings of the Computer Security Foundations Symposium (CSF)"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1214\/aoms\/1177730491"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110259"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738007"},{"key":"e_1_3_1_28_1","first-page":"168","volume-title":"Random Structured Test Data Generation for Black-Box Testing","author":"Pa\u0142ka Micha\u0142 H.","year":"2014","unstructured":"Micha\u0142 H. Pa\u0142ka. 2014. Random Structured Test Data Generation for Black-Box Testing. Department of Computer Science and Engineering, Software Technology (Chalmers), Chalmers University of Technology,. http:\/\/publications.lib.chalmers.se\/records\/fulltext\/195849\/195849.pdf 168."},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1982595.1982615"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2980983.2908093"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547645"},{"key":"e_1_3_1_32_1","doi-asserted-by":"crossref","unstructured":"Jason S. Reich Matthew Naylor and Colin Runciman. 2012. Advances in Lazy SmallCheck. Presented at the 24th Symposium on Implementation and Application of Functional Languages. http:\/\/www.cs.york.ac.uk\/fp\/jason-docs\/ReichNaylorRunciman2013.pdf","DOI":"10.1007\/978-3-642-41582-1_4"},{"key":"e_1_3_1_33_1","volume-title":"Testing of OCaml exceptions by effect-driven generation of programs","author":"Rocha Murilo Giacometti","year":"2019","unstructured":"Murilo Giacometti Rocha. 2019. Testing of OCaml exceptions by effect-driven generation of programs. Master\u2019s thesis. University of Edinburgh. https:\/\/project-archive.inf.ed.ac.uk\/msc\/20193481\/msc_proj.pdf"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17138-4_4"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411286.1411292"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345125"},{"key":"e_1_3_1_37_1","author":"Shirley Peter","year":"2020","unstructured":"Peter Shirley. 2020. Ray Tracing in One Weekend. https:\/\/raytracing.github.io","journal-title":"Ray Tracing in One Weekend"},{"key":"e_1_3_1_38_1","article-title":"On Type-directed Generation of Lambda Terms","author":"Tarau Paul","year":"2015","unstructured":"Paul Tarau. 2015. On Type-directed Generation of Lambda Terms. In Proceedings of the Technical Communications of the 31st International Conference on Logic Programming (ICLP 2015), Cork, Ireland, August 31 - September 4, 2015. http:\/\/ceurws.org\/Vol-1433\/tc_12.pdf","journal-title":"Proceedings of the Technical Communications of the 31st International Conference on Logic Programming (ICLP 2015), Cork, Ireland, August 31 - September 4, 2015"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632919","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632919","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632919","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T18:46:25Z","timestamp":1774982785000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632919"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":38,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632919"],"URL":"https:\/\/doi.org\/10.1145\/3632919","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}