## Andrew W. Appel and Xavier Leroy.
A list-machine benchmark for mechanized metatheory.
Research report 5914, INRIA, 2006.

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.

[ bib |
At HAL |
Local copy ]
Back

*This file was generated by
bibtex2html 1.99.*