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 :
Rapport
[Research Report] RR-5914, INRIA. 2006
Liste complète des métadonnées

https://hal.inria.fr/inria-00077531
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 31 mai 2006 - 10:03:05
Dernière modification le : samedi 17 septembre 2016 - 01:37:30
Document(s) archivé(s) le : lundi 5 avril 2010 - 21:56:37

Fichiers

Identifiants

  • HAL Id : inria-00077531, version 1

Collections

Citation

Andrew W. Appel, Xavier Leroy. A list-machine benchmark for mechanized metatheory. [Research Report] RR-5914, INRIA. 2006. 〈inria-00077531〉

Partager

Métriques

Consultations de
la notice

318

Téléchargements du document

211