A list-machine benchmark for mechanized metatheory

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.
Document type :
Journal articles
Complete list of metadatas

Cited literature [17 references]  Display  Hide  Download

https://hal.inria.fr/hal-00674176
Contributor : Xavier Leroy <>
Submitted on : Saturday, February 25, 2012 - 7:30:22 PM
Last modification on : Friday, May 25, 2018 - 12:02:07 PM
Long-term archiving on : Friday, November 23, 2012 - 2:50:23 PM

File

listmachine-journal.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Andrew Appel, Robert Dockins, Xavier Leroy. A list-machine benchmark for mechanized metatheory. Journal of Automated Reasoning, Springer Verlag, 2012, 49 (3), pp.453--491. ⟨10.1007/s10817-011-9226-1⟩. ⟨hal-00674176⟩

Share

Metrics

Record views

187

Files downloads

267