A List-Machine Benchmark for Mechanized Metatheory
Source: Princeton University
The authors propose a benchmark to compare theorem-proving systems on their ability to express proofs of compiler correctness. In contrast to the first POPL-mark, they emphasize the connection of proofs to compiler implementations, and they point out that much can be done without binders or alpha-conversion. They propose specific criteria for evaluating the utility of mechanized meta-theory systems; they have constructed solutions in both Coq and Twelf meta-theory, and they draw conclusions about those two systems in particular.