Proof Artifacts

Guidelines for Submission and Reviewing


Guidelines for Authors
Guidelines for Reviewers
Additional Resources
Acknowledgments

Introduction

The goal of the proof-artifact evaluation is to recognize and promote high-quality proof artifacts, as well as 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:
    • proofs can be precompiled and submitted on a VM;
    • list the version numbers of the proof assistant and of the libraries that the proof depends on;
    • we recommend to additionally provide instructions on how to build the proof from scratch, preferably in the form of a makefile.
  2. A paper-to-artifact correspondence guide:
    • explain how each of the definitions and theorems in the paper corresponds to the formalizations in the artifact;
    • example:
Definition / Theorem Paper File Name of formalization Notation
Type system of the
simply typed λ-calculus
Page 5,
Figure 2
stlc.v Inductive typing G ⊢ t: T
Preservation Theorem Page 7,
Theorem 1
stlc.v Theorem preservation  
  1. An overview of the libraries and proof frameworks that are used in the proof:
    • explain in what way the proof relies on existing frameworks;
    • the goal is to make the proof readable by a reviewer who is unfamiliar with the frameworks;
    • example:

    This type-safety proof uses the locally nameless representation for terms and cofinite quantification in typing judgements (Aydemir et al., 2008). …

  2. An outline of the proof structure and organization:
    • explain the purpose of the different proof files;
    • optionally, provide a dependency diagram of the proof files.
  3. Document the definitions and important lemmas in the proof:
    • give the main theorems in the proof descriptive names that correspond to their names in the paper;
    • we suggest using tools that generate human-readable documentation (such as coqdoc, isabelle document, Agda documentation, etc.).
  4. Document all places where the proof formalization differs from the paper, for example, through simplifications or alternative definitions;
    • example (formalizing terms of the λ-calculus in Coq):
      Inductive term := 
      ... 
      (** The locally nameless representation represents
       bound variables through de Bruijn indices; therefore
       we can represent an abstraction λx.t as λt’ *)
      | abs : term -> term
      ...
      
  5. Explicitly state and justify all axioms, assumptions, and unfinished parts of the proof:

    We encourage researchers to spend their time on the most important part of the work instead of reproving well-known results. At the same time, given the limited time for reviewing the artifact, it is difficult for the reviewer to assess whether the modified formalization is equivalent to the paper formulation, whether that modification is significant, and whether a lemma with an incomplete proof is obvious.

Guidelines for Reviewers

Additional Resources

Acknowledgments

I would like to thank Robert Rand, Derek Dreyer, Robby Findler, Benjamin Pierce, Stephanie Weirich, Daniel Selsam, Marco Vassena, Daniel Schoepe, Ilya Sergey, Abel Nieto, Ralf Jung, Martin Bodin, Hoang-Hai Dang, Maria Christakis and Philipp Haller for all their feedback which helped greatly improve these guidelines.