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.)
| 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 |
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.
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.
[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>