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

pages

English

Documents

Écrit par
Tobydavis Appel , Andrew Et Al

Publié par
Phuem

Lire

Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres

pages

English

Documents

Lire

Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres

Publié par

Phuem

Nombre de lectures

Langue

English

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 ﬁrst 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 proposespeciﬁc 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 veriﬁcation, 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 diﬃcultto formalize.” The ﬁrst POPLmark examples are all in the theory of F and<:emphasize the theory of binders (e.g., alpha-conversion) ...

Voir

Publié par

Phuem

Langue

English

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

Voir