domains / families / research / popl-artifact-evaluation

popl-artifact-evaluation

separate

Use when packaging a POPL artifact — above all a mechanized proof development in Rocq/Coq, Lean, Agda, or Isabelle — for the post-conditional-acceptance evaluation, satisfying the no-admit/no-sorry completeness rule, mapping paper theorems to proof files, pinning toolchains, and earning the Functional, Reusable, and Available badges.

When to use

• packaging POPL artifacts
• mechanized proof development
• Rocq/Coq proof libraries
• Lean proof libraries
• Agda proof libraries
• Isabelle proof libraries
• satisfying no-admit/no-sorry completeness rule
• mapping paper theorems to proof files

When not to use

• verification tool only
• evaluation harness only

Skill page

Source