Guidelines for Authors
Guidelines for Reviewers
Additional Resources
Acknowledgments
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
To simplify the review process, we suggest that authors include the following in their proof artifacts:
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 |
This type-safety proof uses the locally nameless representation for terms and cofinite quantification in typing judgements (Aydemir et al., 2008). …
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:
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.
(** We assume the four colour theorem
[Chartrand & Lesniak 2005] *)
Axiom four_colour_theorem : ...
(** We extend the logic with functional extensionality,
a well-known axiom that is proved to be consistent
with the calculus of inductive constructions *)
Require Import FunctionalExtensionality.
grep postulate *.agda
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 postulate
or {!!}
in Agda. In Coq, this can be verified using the Print Assumptions
command.
Familiarize yourself with the artifact documentation (proof structure, used frameworks and libraries, representations of data types, stated axioms and hypotheses, etc.) to the extent that is necessary to understand whether the formalizations in the proof and paper are equivalent, modulo the possible deviations that are documented in the paper or artifact.
Compare the definitions and theorems in the paper to the ones in the proof.
Evaluate the artifact based on the following criteria:
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.