POPL Supplementary Material

A POPL submission is really three documents: 25 pages of text (bibliography excluded) that must carry the whole argument, an appendix of full proofs and auxiliary definitions, and — usually — an anonymized proof development or prototype. Reviewers are typically expected to judge the paper from the body alone, so the split is an argumentation decision, not a storage decision. Format and anonymity rules per the POPL 2027 call, read 2026-07-08; confirm the current cycle's supplement wording before uploading.

What lives where

Two disciplines make the split safe:

• The body must stand alone. A reviewer who never opens the appendix should still believe the theorem plausible from the sketch: state the invariant, the hard case, and why it goes through. "Proof in appendix" after an unexplained claim reads as a gap.
• Sketch and proof must not disagree. The classic incident: the body's sketch describes induction on typing derivations while the appendix inducts on evaluation steps because the proof changed. Reviewers who notice stop trusting both.

Anonymizing a proof development

Full double-blind covers everything you upload. Proof repositories are leaky: _CoqProject paths with usernames, lakefile package names matching a public GitHub project, author headers auto-inserted by editors, and .git directories with full commit history. Build the archive from an export, never from a working tree:

git archive --format=tar.gz -o /tmp/supp.tar.gz HEAD          # no .git, no untracked junk
tar tzf /tmp/supp.tar.gz | grep -iE '\.git|/home/|users/|TODO|AUTHORS' && echo LEAK
grep -rInE '(Copyright|Author|@[a-z]+\.(edu|org|fr|de))' \
  --include='*.v' --include='*.lean' --include='*.agda' extracted/ | head

Also rename the development if its public name is googleable to your group, and strip institutional CI configuration.

Version-lock the trio

• Tag the exact commit that generated the submitted PDF, appendix, and archive; the author response will need to quote them line-precisely months later.
• If the appendix is a separate PDF, give it the same section numbering scheme as the body so "App. C.2" resolves unambiguously.
• Late theorem renumbering must propagate to the correspondence table and README — do it with a script, not by hand, in deadline week.

Output format

[Split audit] <claims whose evidence sits only outside the body>
[Sketch-proof consistency] <mismatches found>
[Anonymity scan] clean / leaks listed
[Version lock] <tag/commit for PDF + appendix + archive>
[Upload set] <files, sizes, formats for HotCRP>