Proof Artifacts (ECOOP 2018)

Guidelines for Submission and Reviewing

Marianna Rapoport     Maria Christakis     Philipp Haller
ECOOP Artifacts co-chairs

last updated June 3, 2018

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

• faithfully represents the definitions and theorems in the paper, and
• contains complete proofs for all theorems, without added hypotheses.

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

• it can be reviewed in the allocated time;
• it is straightforward to understand how the mechanized proofs correspond to the definitions and theorems in the paper;
• the proofs of all theorems are complete (except as explained in the paper).

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:
  

3. 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). …

4. 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

5. Document the definitions and important lemmas in the proof

• try to give definitions and lemmas 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.)

6. 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
  ...

7. Explicitly state and justify all axioms, assumptions, and unfinished parts of the proof

• 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
• provide instructions on how to automatically determine what axioms and unproved hypotheses were used
• example:
  To verify that there are no added assumptions, run grep postulate *.agda

Guidelines for Reviewers

• Follow the step-by-step instructions to build the proof.
• Verify that the code compiles.
• Check whether the code contains undocumented assumptions or unfinished proofs, such as the use of “Axiom” or “Admitted” in Coq, “postulate” or “{!!}” in Agda.
• Familiarize yourself with the artifact documentation (proof structure, used frameworks and libraries, representations of data types, etc.) to the extent that is necessary to understand whether the formalizations in the proof and paper are equivalent.
• Compare the definitions and theorems in the paper to the ones in the proof.
• Evaluate the artifact based on the following criteria:

• Readability: Were you able to understand the mechanized definitions and proofs?
• Fidelity: Do the mechanized definitions and proofs correspond precisely to those in the paper? If not, are the points of the departure justified?
• Completeness:  Does the artifact formally verify everything that the paper claims it does?

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, and Derek Dreyer for all their feedback which greatly improved these guidelines.