A List-machine Benchmark for Mechanized Metatheory

LFMTP 2006
A List-machine Benchmark for
Mechanized Metatheory (Extended Abstract)
Andrew W. Appel
Princeton University and INRIA Rocquencourt
Xavier Leroy
INRIA Rocquencourt
Abstract
We propose a benchmark to compare theorem-proving systems on their ability to express proofs of compiler
correctness. In contrast to the first POPLmark, we emphasize the connection of proofs to compiler imple-
mentations, and we point out that much can be done without binders or alpha-conversion. We propose
specific criteria for evaluating the utility of mechanized metatheory systems; we have constructed solutions
in both Coq and Twelf metatheory, and we draw conclusions about those two systems in particular.
Keywords: Theorem proving, proof assistants, program proof, compiler verification, typed machine
language, metatheory, Coq, Twelf.
1 How to evaluate mechanized metatheories
The POPLmark challenge [3] aims to compare the usability of several automated
proof assistants for mechanizing the kind of programming-language proofs that
might be done by the author of a POPL paper, with benchmark problems “chosen
to exercise many aspects of programming languages that are known to be difficult
to formalize.” The first POPLmark examples are all in the theory of F and<:
emphasize the theory of binders (e.g., alpha-conversion).
Practitioners of machine-checked proof about real compilers have interests that
are similar but not identical. We want to formally relate machine-checked proofs
Ato actual ...