Appel, Andrew W.
- Leroy, Xavier
Rapport de recherche de l'INRIA -
Rocquencourt ,
Equipes :
MOSCOVA - GALLIUM
40 pages - Mai 2006 - Document en anglais
Titre français : La list-machine: un exemple de méta-théorie mécanisée
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.
Résumé : Nous proposons un exemple qui permet de comparer des assistants de preuve sur leur capacité à exprimer des preuves de correction de compilateurs. Contrairement au premier défi POPLmark, nous mettons davantage l'accent sur le lien entre les preuves et les implémentations de compilateurs, et moins sur les problèmes soulevés par les lieurs et l'alpha-conversion. Nous proposons des critères précis pour évaluer l'utilité des assistants de preuves dans ce domaine. Nous avons développé des solutions en Coq et en Twelf (métathéorie), et tirons des conclusions à propos de ces deux systèmes en particulier.
Key-Words : THEOREM PROVING / PROOF ASSISTANTS / PROGRAM PROOF / COMPILER VERIFICATION /
TYPED MACHINE LANGUAGE / METATHEORY / COQ / TWELF
Mots-clés : DÉMONSTRATEURS DE THÉORÈMES / ASSISTANTS DE PREUVE / PREUVES DE PROGRAMME /
VÉRIFICATION DE COMPILATEURS / TYPAGE DE CODE MACHINE / MÉTATHÉORIE / COQ /
TWELF
