A list-machine benchmark for mechanized metatheory (extended abstract) - Archive ouverte HAL Access content directly
Conference Papers Year : 2006

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

(1) , (2)
1
2

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.
Fichier principal
Vignette du fichier
listmachine-lfmtp.pdf (175.84 Ko) Télécharger le fichier
Vignette du fichier
Listmachine.v (19.54 Ko) Télécharger le fichier
Vignette du fichier
Listmachine.vo (59.7 Ko) Télécharger le fichier
Vignette du fichier
Maps.v (3.91 Ko) Télécharger le fichier
Vignette du fichier
Maps.vo (20.78 Ko) Télécharger le fichier
Vignette du fichier
README (344 B) Télécharger le fichier
Vignette du fichier
twelf/machine.elf (3.52 Ko) Télécharger le fichier
Vignette du fichier
twelf/proofs.elf (20.09 Ko) Télécharger le fichier
Vignette du fichier
twelf/README (371 B) Télécharger le fichier
Vignette du fichier
twelf/sources.cfg (626 B) Télécharger le fichier
Vignette du fichier
twelf/specification.elf (939 B) Télécharger le fichier
Vignette du fichier
twelf/termination.elf (205 B) Télécharger le fichier
Vignette du fichier
twelf/test.elf (875 B) Télécharger le fichier
Vignette du fichier
twelf/typecheck-proofs.elf (92 B) Télécharger le fichier
Vignette du fichier
twelf/typecheck.elf (790 B) Télécharger le fichier
Vignette du fichier
twelf/types.elf (6.09 Ko) Télécharger le fichier
Vignette du fichier
twelf/unify.elf (870 B) Télécharger le fichier
Origin : Files produced by the author(s)
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Format : Other
Loading...

Dates and versions

inria-00289543 , version 1 (21-06-2008)

Identifiers

Cite

Andrew W. 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. pp.95-108, ⟨10.1016/j.entcs.2007.01.020⟩. ⟨inria-00289543⟩

Collections

INRIA INRIA2 ANR
121 View
113 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More