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

Andrew W. Appel; Xavier Leroy

doi:10.1016/j.entcs.2007.01.020

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

Andrew W. Appel, Xavier Leroy

Research output: Contribution to journal › Article › peer-review

8 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 language	English (US)
Pages (from-to)	95-108
Number of pages	14
Journal	Electronic Notes in Theoretical Computer Science
Volume	174
Issue number	5
DOIs	https://doi.org/10.1016/j.entcs.2007.01.020
State	Published - Jun 2 2007

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
General Computer Science

Keywords

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

Access to Document

10.1016/j.entcs.2007.01.020

Cite this

@article{186ab8782e77471fa9ca31789f12e94a,

title = "A List-machine Benchmark for Mechanized Metatheory. (Extended Abstract)",

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.",

keywords = "Coq, Theorem proving, Twelf, compiler verification, metatheory, program proof, proof assistants, typed machine language",

author = "Appel, {Andrew W.} and Xavier Leroy",

year = "2007",

month = jun,

day = "2",

doi = "10.1016/j.entcs.2007.01.020",

language = "English (US)",

volume = "174",

pages = "95--108",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier",

number = "5",

}

TY - JOUR

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

AU - Appel, Andrew W.

AU - Leroy, Xavier

PY - 2007/6/2

Y1 - 2007/6/2

N2 - 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.

AB - 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.

KW - Coq

KW - Theorem proving

KW - Twelf

KW - compiler verification

KW - metatheory

KW - program proof

KW - proof assistants

KW - typed machine language

UR - http://www.scopus.com/inward/record.url?scp=34249089534&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=34249089534&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2007.01.020

DO - 10.1016/j.entcs.2007.01.020

M3 - Article

AN - SCOPUS:34249089534

SN - 1571-0661

VL - 174

SP - 95

EP - 108

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

IS - 5

ER -

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

Abstract

All Science Journal Classification (ASJC) codes

Keywords

Access to Document

Other files and links

Fingerprint

Cite this