Proof Artifacts (ECOOP 2018)
Guidelines for Submission and Reviewing
Marianna Rapoport Maria Christakis Philipp Haller
ECOOP Artifacts cochairs
last updated June 3, 2018
The goal of a proofartifact 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:
 Stepbystep 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
 A papertoartifact 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

proof/stlc.v

Inductive typing

G ⊢ t : T

Preservation Theorem

Page 7, Theorem 1

proof/stlc.v

Theorem preservation


 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 typesafety proof uses the locally nameless representation for terms and cofinite quantification in typing judgements (Aydemir et al., 2008). …
 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
 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 humanreadable documentation (such as coqdoc, isabelle document, Agda documentation, etc.)
 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
...
 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 stepbystep 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 machinechecked 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.