RECORD
QuickerChick
Programming Languages · Submitted 13 Sep 2026
abstract compiled · 2026-09-23 · no language-model review
The authors' main claim In this work, we describe how we optimized QuickChick, exploiting various opportunities offered by program extraction to significantly improve each test's extraction, compilation, and running time.
The compiled record
The paper's own sentences, arranged. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.
Open the compiled record
The abstract, sentence by sentence
Property-based testing (PBT) with QuickChick relies on extracting Rocq programs to OCaml. However, this extraction mechanism, while crucial for QuickChick to function, has significant performance implications. In this work, we describe how we optimized QuickChick, exploiting various opportunities offered by program extraction to significantly improve each test's extraction, compilation, and running time. We also evaluate these improvements using the ETNA benchmarking platform for PBT to assess how individual improvements impacted the overall test run time.
background contribution method result interpretation main claim
| # | sentence | role | the authors' own work | states the main conclusion | strength |
|---|---|---|---|---|---|
| s0 | Property-based testing (PBT) with QuickChick relies on extracting Rocq programs to OCaml. | background 1.00 | 0.07 | 0.03 | asserted 1.00 |
| s1 | However, this extraction mechanism, while crucial for QuickChick to function, has significant performance implications. | background 0.91 | 0.12 | 0.05 | asserted 1.00 |
| s2 | In this work, we describe how we optimized QuickChick, exploiting various opportunities offered by program extraction to significantly improve each test's extraction, compilation, and running time. | contribution 0.95 | 0.95 | 0.55 | asserted 1.00 |
| s3 | We also evaluate these improvements using the ETNA benchmarking platform for PBT to assess how individual improvements impacted the overall test run time. | method 0.87 | 0.94 | 0.08 | asserted 0.91 |
What was examined, and what was not
- arXiv listing abstract v1
- full text
- figures and tables
- references and citing sentences
- relations to other papers
- P abstract
- S sections
- T body sentences
- C citations
- R cross-paper relations
The paper
Original abstract
Property-based testing (PBT) with QuickChick relies on extracting Rocq programs to OCaml. However, this extraction mechanism, while crucial for QuickChick to function, has significant performance implications. In this work, we describe how we optimized QuickChick, exploiting various opportunities offered by program extraction to significantly improve each test's extraction, compilation, and running time. We also evaluate these improvements using the ETNA benchmarking platform for PBT to assess how individual improvements impacted the overall test run time.
Human review
Discussion
Know something about this paper? Leave a comment, or highlight any passage above to comment on it.