A list-machine benchmark for mechanized metatheory (extended abstract)

Andrew W. Appel 1 Xavier Leroy 2
1 MOSCOVA - Mobililty, security, concurrence, verification and analysis
Inria Paris-Rocquencourt
2 GALLIUM - Programming languages, types, compilation and proofs
Inria Paris-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 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 :
Conference papers
Complete list of metadatas

Cited literature [12 references]  Display  Hide  Download
https://hal.inria.fr/inria-00289543
Contributor : Xavier Leroy <>
Submitted on : Saturday, June 21, 2008 - 1:31:58 PM
Last modification on : Friday, May 25, 2018 - 12:02:07 PM
Long-term archiving on : Friday, September 28, 2012 - 4:25:51 PM

Files

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

Identifiers

Collections

INRIA | INRIA-ROCQ

Citation

Andrew W. Appel, Xavier Leroy. A list-machine benchmark for mechanized metatheory (extended abstract). Int. Workshop on Logical Frameworks and Meta-Languages (LFMTP 2006), Aug 2006, Seattle (Washington), United States. pp.95-108, ⟨10.1016/j.entcs.2007.01.020⟩. ⟨inria-00289543⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

268

Files downloads

146

Contact


archive-ouverte@inria.fr