icalp-reproducibility
GitHub针对ICALP理论论文，通过撰写自包含的完整证明、提供可复现的计算证书及可选的形式化验证，确保结果的可检查性。
Trigger Scenarios
Install
npx skills add brycewang-stanford/Awesome-Journal-Skills --skill icalp-reproducibility -g -y
SKILL.md
Frontmatter
{
"name": "icalp-reproducibility",
"description": "Use when making an ICALP (EATCS) theory result independently checkable — writing complete, self-contained proofs in the appendix and a full version (arXiv\/ECCC\/HAL), pinning any computational steps to reproducible certificates, and (optionally) formalizing key theorems in Coq\/Lean\/Isabelle, since ICALP has no runnable-artifact track and proof verifiability is the analogue of reproducibility."
}
ICALP Reproducibility (proof verifiability and the full version)
At a pure-theory venue, "reproducibility" means a referee — and later any reader — can check the proof. ICALP has no artifact-evaluation track and no badges; the deliverable that plays that role is the full version with complete proofs, plus, where relevant, reproducible computational certificates and optional machine formalization. This skill builds that checkability into the paper from the start, because a proof cannot be reconstructed after the fact any more than a lost dataset can.
The full version is the reproducibility story
- The 15-page body sketches; the full version (a clearly labelled appendix at submission, and an arXiv/ECCC/HAL posting at/after notification) contains every proof in full. This is what makes an ICALP result reproducible: an independent expert can verify it end to end.
- Write proofs self-contained: state every lemma the argument uses, prove or cite each, and avoid "it is easy to see" for steps that are not. The test is whether a competent non-author can follow it without asking you.
- Keep the submission appendix and the eventual arXiv version consistent — divergence between "what the referees checked" and "what is public" undermines trust.
Self-contained proof checklist
[ ] Every theorem's proof is present in full somewhere the referee can read it
[ ] Every lemma used is stated and proved or cited to a precise source
[ ] No "omitted" / "similarly" hiding a genuinely hard case
[ ] Constants and asymptotics are traceable (no unexplained factor changes mid-proof)
[ ] Definitions precede use; notation is defined once and used consistently
[ ] The dependency structure of lemmas is clear (nothing circular)
Reproducible computation, when a proof uses it
If a proof relies on computation (see icalp-experiments), the computation must be checkable, not
merely asserted:
- Ship code and inputs, or precise pseudocode, in the full version or a referenced public repo.
- Prefer an independently verifiable certificate (UNSAT proof, LP/Farkas witness, explicit witness object) over "our program confirms it."
- Pin solver versions and any random seeds so the check is deterministic.
Optional: machine-checked formalization
ICALP does not require formalization, but a Coq/Lean/Isabelle proof of a central theorem is a strong, increasingly valued signal — especially for intricate combinatorial or semantic arguments:
- Formalize the load-bearing theorem, not the whole paper, and say precisely what is formalized and what is assumed (axioms, unformalized lemmas).
- Archive the development (a public repo, or Software Heritage / Zenodo for a DOI) and reference it in the camera-ready. Do not let it break anonymity during review.
- Be honest about the gap between the paper's statement and the formal statement; an over-claimed formalization is worse than none.
What ICALP reproducibility is NOT
- It is not a runnable-system artifact, a Docker image of an implementation, or a benchmark
harness — there is no artifact track and no badge to earn (
icalp-artifact-evaluationexplains the distinction). - It is not "available upon request." A proof that only the authors can complete is, for review purposes, not a proof.
- It is not satisfied by an arXiv link alone if that version, too, defers the hard steps.
Worked vignette: an intricate lower bound
A Track A conditional lower bound hinges on a delicate gadget construction. To make it reproducible: prove the gadget's properties in full in the appendix (not "by inspection"); include a small computer-checked verification of the gadget's truth table with a shipped, re-runnable script and its output; post an arXiv full version at notification identical in content to the checked appendix; and, optionally, formalize the core combinatorial lemma in Lean and cite the archived development at camera-ready. State clearly which parts are machine-checked.
Output format
[Full version] complete proofs present (appendix now, arXiv at notification)? gaps: <where>
[Self-containment] lemmas stated+proved/cited; no hidden hard cases? yes/no
[Computation] certificates / reproducible inputs provided where a proof uses computation? n/a or yes/no
[Formalization] none / partial (what theorem, what assumed) / archived+cited
[Anonymity] full version / repo referenced without breaking the blind during review? yes/no
[Fix queue] <ordered: proof completeness, certificates, formalization scope>
Version History
- 9f86f09 Current 2026-07-19 15:53
