A list-machine benchmark for mechanized metatheory (extended abstract)

Andrew W. Appel 1 Xavier Leroy 2
1 MOSCOVA - Mobililty, security, concurrence, verification and analysis
Inria Paris-Rocquencourt
2 GALLIUM - Programming languages, types, compilation and proofs
Inria Paris-Rocquencourt
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 :
Communication dans un congrès
Int. Workshop on Logical Frameworks and Meta-Languages (LFMTP 2006), Aug 2006, Seattle (Washington), United States. Elsevier, 174/5, pp.95-108, 2006, Electronic Notes in Theoretical Computer Science. 〈10.1016/j.entcs.2007.01.020〉
Liste complète des métadonnées

Littérature citée [12 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/inria-00289543
Contributeur : Xavier Leroy <>
Soumis le : samedi 21 juin 2008 - 13:31:58
Dernière modification le : vendredi 25 mai 2018 - 12:02:07
Document(s) archivé(s) le : vendredi 28 septembre 2012 - 16:25:51

Fichiers

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

Identifiants

Collections

INRIA

Citation

Andrew W. Appel, Xavier Leroy. A list-machine benchmark for mechanized metatheory (extended abstract). Int. Workshop on Logical Frameworks and Meta-Languages (LFMTP 2006), Aug 2006, Seattle (Washington), United States. Elsevier, 174/5, pp.95-108, 2006, Electronic Notes in Theoretical Computer Science. 〈10.1016/j.entcs.2007.01.020〉. 〈inria-00289543〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

234

Téléchargements de fichiers

139

Contact


archive-ouverte@inria.fr