popl-artifact-evaluation
GitHub指导POPL论文作者打包形式化证明（Coq/Lean等）以供评估。确保无admit/sorry，完成公理审计，固定工具链，建立声明映射，并提供快速构建指南以获取功能、可复用和可用徽章。
触发场景
安装
npx skills add brycewang-stanford/Awesome-Journal-Skills --skill popl-artifact-evaluation -g -y
SKILL.md
Frontmatter
{
"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:
# 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 wheremakejust works. - Map claims to files. A
CORRESPONDENCE.mdtable — paper theorem number, formal statement name, file, line — is the single highest-leverage document (popl-reproducibilitymaintains 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 quickthat 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>
版本历史
- 9f86f09 当前 2026-07-19 17:17
