brycewang-stanford 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>