A List-Machine Benchmark for Mechanized Metatheory

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

Full description

Saved in:
Bibliographic Details
Published in:Journal of automated reasoning 2012-10, Vol.49 (3), p.453-491
Main Authors: Appel, Andrew W., Dockins, Robert, Leroy, Xavier
Format: Article
Language:English
Subjects:
Artificial Intelligence
Benchmarking
Binders
Compilers
Computer Science
Construction specifications
Criteria
Joints
Mathematical Logic and Formal Languages
Mathematical Logic and Foundations
Programming Languages
Proving
Symbolic and Algebraic Manipulation
Utilities
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0168-7433
1573-0670
DOI:10.1007/s10817-011-9226-1