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