popl-reproducibility

POPL Reproducibility

At a theory venue "reproducible" does not mean rerunnable seeds; it means **an

independent reader can re-establish your claims**. For POPL that decomposes by claim

type, and the discipline pays twice: once with reviewers under full double-blind, and

again with artifact evaluators after conditional acceptance, where reusable proof

claims must be complete — no admit, no sorry (AE criteria read 2026-07-08).

What each claim type owes the reader

| Claim type | Its reproducibility obligation |

|---|---|

| Mechanized theorem | Development compiles; theorem checkable; axioms printed and declared |

| On-paper theorem | Full proof in the appendix; every hypothesis stated where used, not discovered mid-proof |

| Definitional adequacy ("our semantics models X") | Examples or an adequacy theorem connecting formalism to the informal system |

| Prototype measurement | Scripted runs, versioned inputs, stated machine — see popl-experiments |

Mechanize deliberately, not maximally

Full mechanization is powerful but not free; partial mechanization is respectable at

POPL when scoped honestly. Decide per theorem:

• Mechanize the theorems whose proofs are long, syntactic, and error-prone — subject

reduction, soundness of a logical relation — where hand-proof mistakes hide.

• Hand-prove what is short and conceptual, and write the proof in full; "routine

induction" is a claim reviewers test by attempting the induction.

• Never let paper and mechanization silently diverge: if the mechanized calculus

drops polymorphism, the paper's theorem statement must say so.

• Statement drift is the classic failure — the .v file proves a lemma about a

judgment the paper revised two drafts ago.

The correspondence table

Start this file the week the first lemma lands, not the week AE starts:

| Paper stmt | Formal name | File:line | Status | Axioms |
|---|---|---|---|---|
| Thm 3.1 (soundness) | `soundness` | theories/Sound.v:212 | Qed | none |
| Lem 3.2 (subst) | `subst_pres` | theories/Subst.v:88 | Qed | funext (declared) |
| Thm 5.4 (full abstraction) | — | on-paper only, App. D | complete proof | classical logic |

Regenerate the status column mechanically (grep -c "Admitted" theories/*.v should

be zero or explained) and cite the table in the paper's contributions paragraph — it

is the sentence "all results are mechanized except Thm 5.4" made auditable.

Assumption hygiene for on-paper proofs

• Number global assumptions once (Assumption 1, 2, ...) and cite them by number in

every theorem; unnumbered ambient hypotheses are where soundness doubts breed.

• Keep one notation table; a symbol that changes meaning between Section 3 and

Appendix B costs a review cycle.

• When a proof cites "standard techniques," name the technique and the source

theorem — the reader must be able to find the exact statement being invoked.

• Archive the appendix, proofs, and development in the same repository so a revision

to one forces a visible diff in the others.

Output format

[Claim inventory] mechanized:<n> on-paper:<n> empirical:<n>
[Correspondence table] exists / stale / missing
[Divergences] <paper statement vs formalization deltas, each disclosed?>
[Assumption hygiene] <numbered? notation table? invoked-theorem citations?>
[Weakest link] <the one claim an independent reader cannot currently re-establish>