| 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-evaluation explains 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>
