popl-artifact-evaluation

POPL Artifact Evaluation

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?"

The badge criteria, proof-flavored

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

The axiom audit

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.

Package for an evaluator with one week and one laptop

• Pin the toolchain. Proof assistants break across versions: fix the Rocq/Coq

release via opam switch or the Lean toolchain via lean-toolchain, and ship a

container or VM where make just works.

• Map claims to files. A CORRESPONDENCE.md table — paper theorem number,

formal statement name, file, line — is the single highest-leverage document

(popl-reproducibility maintains it from submission onward).

• Budget honest times. Say that the full build takes 90 minutes and the

kick-the-tires target takes 5; give a make quick that checks one headline

theorem.

• State the deltas. Where the mechanization simplifies the paper (a smaller

calculus, a restricted case), say so in the README before the evaluator finds out.

• Archive the exact evaluated snapshot on Zenodo for the Available badge, and keep

developing in the live repository afterward.

Output format

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