[inria-00289543, v1] A list-machine benchmark for mechanized metatheory (extended abstract)

Tobydavis Appel, Andrew Et Al

Description

Author manuscript, published in "Int. Workshop on Logical Frameworks and Meta-Languages (LFMTP 2006), Seattle(Washington) : United States (2006)" DOI : 10.1016/j.entcs.2007.01.020LFMTP 2006A List-machine Benchmark forMechanized Metatheory (Extended Abstract)Andrew W. AppelPrinceton University and INRIA RocquencourtXavier LeroyINRIA RocquencourtAbstractWe propose a benchmark to compare theorem-proving systems on their ability to express proofs of compilercorrectness. In contrast to the first POPLmark, we emphasize the connection of proofs to compiler imple-mentations, and we point out that much can be done without binders or alpha-conversion. We proposespecific criteria for evaluating the utility of mechanized metatheory systems; we have constructed solutionsin both Coq and Twelf metatheory, and we draw conclusions about those two systems in particular.Keywords: Theorem proving, proof assistants, program proof, compiler verification, typed machinelanguage, metatheory, Coq, Twelf.1 How to evaluate mechanized metatheoriesThe POPLmark challenge [3] aims to compare the usability of several automatedproof assistants for mechanizing the kind of programming-language proofs thatmight be done by the author of a POPL paper, with benchmark problems “chosento exercise many aspects of programming languages that are known to be difficultto formalize.” The first POPLmark examples are all in the theory of F and<:emphasize the theory of binders (e.g., alpha-conversion) ...

Informations

• Publié par: Phuem
• Nombre de lectures: 26
• Langue: English

Extrait

Author manuscript, published in "Int. Workshop on Logical Frameworks and Meta-Languages (LFMTP 2006), Seattle (Washington) : United States (2006)" DOI : 10.1016/j.entcs.2007.01.020