POPL invites authors of conditionally accepted papers to submit supporting materials to artifact evaluation, and its AE tracks treat proof developments as the canonical artifact: Coq and Isabelle proof libraries are the track's own examples of reusable artifacts (POPL 2025/2026 AE pages, read 2026-07-08). A verification tool or evaluation harness can ride along, but at this venue the evaluator's core question is usually "does this mechanization actually prove what the paper claims?"
| Badge | Criterion (2025/2026 wording) | For a proof artifact this means |
|---|---|---|
| Artifacts Evaluated - Functional | Supports the paper's claims, documented well enough to run and validate | The development compiles from scratch and each paper theorem is checkable |
| Artifacts Evaluated - Reusable | Additionally packaged for reuse: docs, installation, portability, new examples, open licensing / issue tracker | Definitions and lemmas usable by other projects — and complete: no admit in Coq/Rocq, no sorry in Lean or Isabelle |
| Artifacts Available | Archived eternally on an archival repository (Zenodo, ACM DL) | A DOI-stamped snapshot; a lab GitHub URL is not archival |
The completeness rule is the sharpest tooth: a single admitted lemma demotes a "reusable" claim, and evaluators grep for it.
Closing all goals is not enough — evaluators also ask what the development assumes. Print the axiom footprint of every top-level theorem and disclose it in the README:
# Rocq/Coq: full consistency check plus per-theorem assumptions
coqchk -silent -o MyDev.Main
echo "Print Assumptions main_soundness." | coqtop -l theories/Main.v
# Lean 4: elaborate and show axioms
lake build && echo '#print axioms Main.soundness' >> Scratch.lean
# Agda: flag unfinished holes and postulates
grep -rn "postulate" src/ ; agda --safe src/Everything.agda
Classical axioms, functional extensionality, or proof irrelevance are usually acceptable when declared; an undeclared axiom discovered by the evaluator is a credibility wound.
lean-toolchain, and ship a
container or VM where make just works.CORRESPONDENCE.md table — paper theorem number,
formal statement name, file, line — is the single highest-leverage document
(popl-reproducibility maintains it from submission onward).make quick that checks one headline
theorem.[Artifact type] proof development / tool + proofs / tool only
[Completeness] admits: <n> sorries: <n> postulates: <n> (target: 0 declared-only)
[Axiom footprint] <per main theorem>
[Correspondence] <paper theorems mapped / total>
[Badge readiness] Functional: <y/n> Reusable: <y/n> Available: <DOI or missing>