--- 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 ```text [ ] 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 ```text [Full version] complete proofs present (appendix now, arXiv at notification)? gaps: [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] ```