A list-machine benchmark for mechanized metatheory

Andrew W. Appel, Robert Dockins, Xavier Leroy

Research output: Contribution to journalArticlepeer-review

7 Scopus citations


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.

Original languageEnglish (US)
Pages (from-to)453-491
Number of pages39
JournalJournal of Automated Reasoning
Issue number3
StatePublished - Oct 2012

All Science Journal Classification (ASJC) codes

  • Software
  • Computational Theory and Mathematics
  • Artificial Intelligence


  • Compiler verification
  • Coq
  • Metatheory
  • Program proof
  • Proof assistants
  • Theorem proving
  • Twelf
  • Typed machine language


Dive into the research topics of 'A list-machine benchmark for mechanized metatheory'. Together they form a unique fingerprint.

Cite this