A list-machine benchmark for mechanized metatheory

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.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2012, 49 (3), pp.453--491. 〈10.1007/s10817-011-9226-1〉
Liste complète des métadonnées

Littérature citée [17 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00674176
Contributeur : Xavier Leroy <>
Soumis le : samedi 25 février 2012 - 19:30:22
Dernière modification le : jeudi 10 janvier 2013 - 23:17:25
Document(s) archivé(s) le : vendredi 23 novembre 2012 - 14:50:23

Fichier

listmachine-journal.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Andrew Appel, Robert Dockins, Xavier Leroy. A list-machine benchmark for mechanized metatheory. Journal of Automated Reasoning, Springer Verlag, 2012, 49 (3), pp.453--491. 〈10.1007/s10817-011-9226-1〉. 〈hal-00674176〉

Partager

Métriques

Consultations de
la notice

121

Téléchargements du document

139