Making our Own Luck: A Language for Random Generators
QuickCheck-style property-based random testing requires efficient generators for well-distributed random data satisfying complex logical predicates. Writing such generators by hand can be difficult and error prone.
We propose a domain-specific language, Luck, in which generators are expressed by decorating predicates with lightweight annotations controlling both the distribution of generated values and the amount of constraint solving that happens before each variable is instantiated. Generators in Luck are compact, readable, and maintainable, with efficiency close to custom handwritten generators.
We give a precise denotational semantics for Luck, reminiscent of those of probabilistic programming languages, and prove key theorems about its behavior, including the soundness and completeness of random generation with respect to a straightforward predicate semantics. We evaluate Luck on a collection of common examples from the random testing literature and on two significant case studies showing how Luck can be used for complex bug-finding tasks with comparable effectiveness and an order of magnitude reduction in testing code size, compared to handwritten generators.
Sat 23 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
14:00 - 15:30
|A Lambda-Calculus Foundation for Universal Probabilistic Programming|
Johannes Borgström Uppsala University, Ugo Dal Lago University of Bologna, Andrew D. Gordon Microsoft Research and University of Edinburgh, Marcin Szymczak University of EdinburghPre-print
|Making our Own Luck: A Language for Random Generators|
Leonidas Lampropoulos University of Pennsylvania, Benjamin C. Pierce University of Pennsylvania, Cătălin Hriţcu INRIA Paris, John Hughes Chalmers University of Technology, Zoe Paraskevopoulou Princeton University, Li-yao Xia ENS ParisPre-print
|Semantics of Higher-order Probabilistic Programs|
Sam Staton University of Oxford, Hongseok Yang University of Oxford, UK, Chris Heunen University of Edinburgh, Ohad Kammar University of Cambridge, Frank Wood University of OxfordPre-print