A list-machine benchmark for mechanized metatheory
by Andrew W. Appel, Robert Dockins, and Xavier Leroy. To appear in Journal of Automated Reasoning, estimated 2011 or 2012.
Earlier versions:A list-machine benchmark for mechanized metatheory
by Andrew W. Appel and Xavier Leroy. INRIA Research Report RR-5914, May 2006. A shorter version appeared in LFMTP'06: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, August 2006.
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 implementations, 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.
List-machine exercise We provide Coq and Twelf solutions to the benchmark with most proofs and some supporting lemmas removed. They can be used as an exercise in learning Coq or Twelf.
Semantic and syntactic proofs for the List Machine
by Andrew W. Appel and Robert Dockins April 2006
We demonstrate two Coq developments of the List Machine type-soundness proof, a syntactic proof and a modal semantic proof. The syntactic proof is similar to that described by Appel and Leroy (2006); the semantic proof uses a modal style, as described in this paper:
Multimodal Separation Logic for Reasoning About Operational Semantics, by Robert Dockins, Andrew W. Appel, and Aquinas Hobor, (to appear) in Twenty-fourth Conference on the Mathematical Foundations of Programming Semantics, May 2008.