| name | popl-experiments |
| description | Use when designing the empirical component of a POPL paper — deciding whether evidence should be a mechanization, a prototype, case studies, or benchmarks; reporting proof effort and case-study coverage honestly; and keeping performance numbers in a supporting role so the formal claim stays the paper's center of gravity. |
POPL Experiments and Empirical Evidence
POPL welcomes experimental papers, but the evaluation's job differs from a systems
venue: at POPL, evidence demonstrates that the formal idea is realizable and
relevant, it does not substitute for the theorem. Calibrate the empirical section
to the claim it supports, and no further. (Venue facts referenced here were checked
2026-07-08; see resources/official-source-map.md.)
Match evidence to claim
| Claim in the paper | Right evidence | Wrong evidence |
|---|
| "The type system is sound" | Proof (mechanized or on-paper, popl-reproducibility) | A test suite that found no counterexample |
| "The analysis is precise enough to be useful" | Case studies on real programs with found/missed counts | One toy example |
| "The logic scales to real proofs" | Proof effort data: LOC, person-time, lemma reuse across case studies | Adjectives ("lightweight," "practical") |
| "Checking is fast enough for interaction" | Timings on stated hardware with input sizes | Asymptotic claims dressed as measurements |
| "The translation preserves behavior" | The theorem, plus differential testing as a sanity layer | Testing alone |
Proof effort is data at this venue
Papers about logics, tactics, and frameworks make usability claims; the honest
currency is effort accounting. Report it like a measurement, mechanically:
coqwc theories/*.v | tail -5
grep -rcE '^(theorem|lemma|def) ' Src/ | sort -t: -k2 -nr | head
State what the numbers do not show: person-days depend on author expertise, and
line counts are assistant-specific. An honest caveat paragraph here reads as
maturity, not weakness.
Case-study discipline
- Choose case studies that stress different features of the formalism, and say
which feature each exercises; three variations on one pattern count as one.
- Report failures and near-misses: the program the analysis could not verify, the
proof that needed a manual bridge lemma. POPL reviewers trust evaluations that
contain bad news.
- Distinguish the artifact language from the ambient claim: results for a core
calculus fragment must not be narrated as results for the full language.
- If a baseline tool exists, compare capability first (what each can express or
verify) and performance second.
Performance numbers, when present
Keep them survivable rather than spectacular: fixed machine spec, versioned inputs,
repeated runs with dispersion, scripts in the artifact so evaluators can regenerate
every table (popl-artifact-evaluation). A slow but sound prototype is publishable
at POPL; an irreproducible speedup claim is a liability everywhere.
Output format
[Claim-evidence map] <each empirical claim -> its evidence type; mismatches flagged>
[Effort accounting] <LOC/person-time/case-study table present? caveats stated?>
[Bad-news audit] <failures and limitations reported, or missing>
[Regenerability] <scripts + machine spec + versions for every number>
