domains / families / research / popl-reproducibility

popl-reproducibility

separate

Use when making a POPL paper's results independently checkable — deciding which theorems to mechanize versus hand-prove, maintaining a paper-to-proof correspondence table from day one, keeping on-paper proofs auditable with explicit assumption tracking, and making any accompanying prototype's numbers regenerable.

When to use

• deciding which theorems to mechanize versus hand-prove
• maintaining a paper-to-proof correspondence table
• keeping on-paper proofs auditable with explicit assumption tracking
• making accompanying prototype's numbers regenerable
• tracking divergences between paper statements and formalizations
• ensuring assumption hygiene for on-paper proofs

When not to use

• rerunnable seeds
• maximal mechanization without honest scoping

Skill page

Source