| name | popl-artifact-evaluation |
| description | Use when packaging a POPL artifact — above all a mechanized proof development in Rocq/Coq, Lean, Agda, or Isabelle — for the post-conditional-acceptance evaluation, satisfying the no-admit/no-sorry completeness rule, mapping paper theorems to proof files, pinning toolchains, and earning the Functional, Reusable, and Available badges. |
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:
coqchk -silent -o MyDev.Main
echo "Print Assumptions main_soundness." | coqtop -l theories/Main.v
lake build && echo '#print axioms Main.soundness' >> Scratch.lean
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>
