popl-experiments

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:

# Rocq/Coq development: spec vs proof line counts per file
coqwc theories/*.v | tail -5
# Lean 4: declaration counts as a proxy for library size
grep -rcE '^(theorem|lemma|def) ' Src/ | sort -t: -k2 -nr | head
# Case-study table skeleton: program, LOC, proved property, person-days, reused lemmas

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>