Proof Artifacts

Guidelines for Submission and Reviewing

Marianna Rapoport     Maria Christakis     Philipp Haller

last updated March 21, 2018

The goal of a proof-artifact review is to verify that the mechanized formalization of a paper

Authors should organize and document their artifact sufficiently to ensure that a reviewer can complete their assessment within one day.

Reviewers will be aiming to accept the artifact if

Guidelines for Authors

To simplify the review process, we suggest that authors include the following in their proof artifacts:

  1. Step-by-step instructions on how to build and compile the proof
  1. A paper-to-artifact correspondence guide

Definition / Theorem

Paper

File

Name of formalization

Notation

Type system of the simply typed

λ-calculus

Page 5,
Figure 2

proof/stlc.v

Inductive typing

G ⊢ t : T

Preservation Theorem

Page 7, Theorem 1

proof/stlc.v

Theorem preservation

  1. An overview of the libraries and proof frameworks that are used in the proof
  1. An outline of the proof structure and organization
  1. Document the definitions and important lemmas in the proof
  1. Document all places where the proof formalization differs from the paper, for example, through simplifications or alternative definitions
  1. Explicitly state and justify all axioms, assumptions, and unfinished parts of the proof

Guidelines for Reviewers

Additional Resources

How to review formalized mathematics

Checking machine-checked proofs

Guidelines for Packaging AEC Submissions

About Artifact Evaluation

Acknowledgments

We would like to thank Robert Rand, Robby Findler, Benjamin Pierce, Daniel Selsam, Marco Vassena, Daniel Schoepe, Ilya Sergey, Derek Dreyer, Matthias Hauswirth, and Shriram Krishnamurthi for all their feedback which greatly improved these guidelines.