{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,28]],"date-time":"2026-07-28T13:02:30Z","timestamp":1785243750879,"version":"3.55.0"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1421243,1521523,1407794"],"award-info":[{"award-number":["1421243,1521523,1407794"]}],"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":[[2018,1]]},"abstract":"<jats:p>Property-based random testing (PBRT) is widely used in the functional programming and verification communities. For testing simple properties, PBRT tools such as QuickCheck can automatically generate random inputs of a given type. But for more complex properties, effective testing often demands generators for random inputs that belong to a given type and satisfy some logical condition. QuickCheck provides a library of combinators for building such generators by hand, but this can be tedious for simple conditions and error prone for more complex ones. Fortunately, the process can often be automated. The most prominent method, narrowing, works by traversing the structure of the condition, lazily instantiating parts of the data structure as constraints involving them are met.<\/jats:p>\n          <jats:p>We show how to use ideas from narrowing to compile a large subclass of Coq's inductive relations into efficient generators, avoiding the interpretive overhead of previous implementations. More importantly, the same compilation technique allows us to produce proof terms certifying that each derived generator is good---i.e., sound and complete with respect to the inductive relation it was derived from. We implement our algorithm as an extension of QuickChick, an existing tool for property-based testing in Coq. We evaluate our method by automatically deriving good generators for the majority of the specifications in Software Foundations, a formalized textbook on programming language foundations.<\/jats:p>","DOI":"10.1145\/3158133","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":37,"title":["Generating good generators for inductive relations"],"prefix":"10.1145","volume":"2","author":[{"given":"Leonidas","family":"Lampropoulos","sequence":"first","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zoe","family":"Paraskevopoulou","sequence":"additional","affiliation":[{"name":"Princeton University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Benjamin C.","family":"Pierce","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/347476.347484"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411273.1411275"},{"key":"e_1_2_2_3_1","volume-title":"2nd International Conference on Certified Programs and Proofs (CPP) (Lecture Notes in Computer Science)","volume":"7679","author":"Bulwahn Lukas","year":"2012"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28717-6_14"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29578-2_9"},{"key":"e_1_2_2_6_1","volume-title":"Integrating Testing and Interactive Theorem Proving. In 10th International Workshop on the ACL2 Theorem Prover and its Applications (EPTCS)","volume":"70","author":"Chamarthi Harsh Raju","year":"2011"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78969-7_23"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07151-0_2"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74591-4_7"},{"key":"e_1_2_2_11_1","volume-title":"The Coq Workshop. (July","author":"D\u00e9n\u00e8s Maxime","year":"2014"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/10930755_12"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2004.07.002"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_16"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273920.1273930"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806835"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2009.10"},{"key":"e_1_2_2_18_1","volume-title":"Proc. ILPS\u201995 Workshop on Visions for the Future of Logic Programming. 95\u2013107","author":"Hanus M."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500574"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000058"},{"key":"e_1_2_2_21_1","volume-title":"QuickCheck Testing for Fun and Profit. In 9th International Symposium on Practical Aspects of Declarative Languages (PADL) (Lecture Notes in Computer Science)","volume":"4354","author":"Hughes John","year":"2007"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2010.62"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2637647.2637655"},{"key":"e_1_2_2_24_1","volume-title":"OOPSLA","author":"Kuraj Ivan"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009868"},{"key":"e_1_2_2_26_1","volume-title":"Property Directed Generation of First-Order Test Data. In 8th Symposium on Trends in Functional Programming (Trends in Functional Programming)","volume":"8","author":"Lindblad Fredrik","year":"2007"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297846.1297902"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1982595.1982615"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034654.2034663"},{"key":"e_1_2_2_30_1","volume-title":"Foundational Property-Based Testing. In 6th International Conference on Interactive Theorem Proving (ITP) (Lecture Notes in Computer Science), Christian Urban and Xingyuan Zhang (Eds.)","volume":"9236","author":"Paraskevopoulou Zoe"},{"key":"e_1_2_2_31_1","volume-title":"Chris Casinghino, Marco Gaboardi, Michael Greenberg, C\u0103t\u0103lin Hri\u0163cu, Vilhelm Sj\u00f6berg, and Brent Yorgey.","author":"Pierce Benjamin C.","year":"2016"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054170"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411286.1411292"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_33"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_9"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75283"},{"key":"e_1_2_2_38_1","unstructured":"Li-yao Xia. 2017. generic-random: Generic Customizable Arbitrary Instances. http:\/\/hackage.haskell.org\/package\/ generic- random . (10 April 2017).  Li-yao Xia. 2017. generic-random: Generic Customizable Arbitrary Instances. http:\/\/hackage.haskell.org\/package\/ generic- random . (10 April 2017)."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158133","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158133","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158133","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158133"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":38,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158133"],"URL":"https:\/\/doi.org\/10.1145\/3158133","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}