Reference. Programmable Property-Based Testing

Property-based testing (PBT) is a popular technique for establishing confidence in software, where users write properties —i.e. executable specifications—that can be checked many times in a loop by a testing framework. In modern PBT frameworks, properties are usually written in shallowly embedded domain-specific languages, and their definition is tightly coupled to the way they are tested. Such frameworks often provide convenient configuration options to customize aspects of the testing process, but users are limited to precisely what library authors had the prescience to allow for when developing the framework; if they want more flexibility, they may need to write a new framework from scratch. We propose a new, deeper language for properties based on a mixed embedding that we call deferred binding abstract syntax , which reifies properties as a data structure and decouples them from the property runners that execute them. We implement this language in Rocq and Racket, leveraging the power of dependent and dynamic types, respectively. Finally, we showcase the flexibility of this new approach by implementing a variety of property runners in a shared framework, highlighting domain-specific testing improvements that can be unlocked by more programmable testing.

Cite

Cite as @keles-2026-programmable (helia, typst) · \cite{keles-2026-programmable} (LaTeX)
BibTeX
bibtex · 1 line
@article{keles-2026-programmable, title={Programmable Property-Based Testing}, volume={10}, ISSN={2475-1421}, url={http://dx.doi.org/10.1145/3828685}, DOI={10.1145/3828685}, number={ICFP}, journal={Proceedings of the ACM on Programming Languages}, publisher={Association for Computing Machinery (ACM)}, author={Keles, Alperen and Frank, Justine and Mert, Ceren and Goldstein, Harrison and Lampropoulos, Leonidas}, year={2026}, month=Aug, pages={365–396} }
hayagriva YAML (typst)
yaml · 21 lines
keles-2026-programmable:
  type: article
  title: Programmable Property-Based Testing
  author:
  - Keles, Alperen
  - Frank, Justine
  - Mert, Ceren
  - Goldstein, Harrison
  - Lampropoulos, Leonidas
  date: 2026-08
  page-range: 365-396
  url: http://dx.doi.org/10.1145/3828685
  serial-number:
    doi: 10.1145/3828685
    issn: 2475-1421
  parent:
    type: periodical
    title: Proceedings of the ACM on Programming Languages
    publisher: Association for Computing Machinery (ACM)
    issue: ICFP
    volume: 10
Cites 50 works (2 here)
With notes (2)

Finding and Understanding Bugs in C Compilers yangFindingUnderstandingBugs

Compilers should be correct. To improve the quality of C compilers, we created Csmith, a randomized test-case generation tool, and spent three years using it to find compiler bugs. During this period we reported more than 325 previously unknown bugs to compiler developers. Every compiler we tested was found to crash and also to silently generate wrong code when presented with valid input. In this paper we present our compiler-testing tool and the results of our bug-hunting study. Our first contribution is to advance the state of the art in compiler testing. Unlike previous tools, Csmith generates programs that cover a large subset of C while avoiding the undefined and unspecified behaviors that would destroy its ability to automatically find wrong-code bugs. Our second contribution is a collection of qualitative and quantitative results about the bugs we have found in open-source C compilers.
PDF · DOI · pldb

Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages carette-2009-finally

We have built the first family of tagless interpretations for a higher-order typed object language in a typed metalanguage (Haskell or ML) that require no dependent types, generalized algebraic data types, or postprocessing to eliminate tags. The statically type-preserving interpretations include an evaluator, a compiler (or staged evaluator), a partial evaluator, and call-by-name and call-by-value continuation-passing style (CPS) transformers. Our principal technique is to encode de Bruijn or higher-order abstract syntax using combinator functions rather than data constructors. In other words, we represent object terms not in an initial algebra but using the coalgebraic structure of the λ-calculus. Our representation also simulates inductive maps from types to types, which are required for typed partial evaluation and CPS transformations. Our encoding of an object term abstracts uniformly over the family of ways to interpret it, yet statically assures that the interpreters never get stuck. This family of interpreters thus demonstrates again that it is useful to abstract over higher-kinded types.
PDF · DOI · pldb
External (48)
keles-2026-programmable reference entries/refs/keles-2026-programmable/keles-2026-programmable.hel