| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
A list-machine benchmark for mechanized metatheory (extended abstract)
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.
Cited literature [12 references]
https://hal.inria.fr/inria-00289543
Contributor : Xavier Leroy Connect in order to contact the contributor
Submitted on : Saturday, June 21, 2008 - 1:31:58 PM
Last modification on : Thursday, February 3, 2022 - 11:14:19 AM
Long-term archiving on: : Friday, September 28, 2012 - 4:25:51 PM
Contributor : Xavier Leroy Connect in order to contact the contributor
Submitted on : Saturday, June 21, 2008 - 1:31:58 PM
Last modification on : Thursday, February 3, 2022 - 11:14:19 AM
Long-term archiving on: : Friday, September 28, 2012 - 4:25:51 PM