| name | popl-supplementary |
| description | Use when splitting a POPL paper across the 25-page body, the proof appendix, and anonymous supplementary material — deciding which proofs and auxiliary judgments leave the text, packaging proof scripts without identity leaks under full double-blind, and keeping every artifact self-consistent with the submission PDF. |
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
| Content | Body (25 pp) | Appendix | Anonymous artifact |
|---|
| Main definitions, typing/semantics rules actually discussed | yes | mirrored in full | formalized |
| Main theorem statements + proof sketches | yes | full proofs | checked statements |
| Auxiliary lemmas, weakening/substitution boilerplate | no | yes | yes |
| Full figure of every judgment (all rules) | representative rules only | complete figure | source of truth |
| Extended examples, failed design alternatives | one motivating example | yes | test files |
| Proof scripts, build instructions | no | no | yes, with README |
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
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>
