A List-machine Benchmark for Mechanized Metatheory. (Extended Abstract)

Andrew W. Appel, Xavier Leroy

Research output: Contribution to journalArticle

4 Scopus citations

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.

Original languageEnglish (US)
Pages (from-to)95-108
Number of pages14
JournalElectronic Notes in Theoretical Computer Science
Volume174
Issue number5
DOIs
StatePublished - Jun 2 2007

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Keywords

  • Coq
  • Theorem proving
  • Twelf
  • compiler verification
  • metatheory
  • program proof
  • proof assistants
  • typed machine language

Fingerprint Dive into the research topics of 'A List-machine Benchmark for Mechanized Metatheory. (Extended Abstract)'. Together they form a unique fingerprint.

Cite this