Documents

37 pages

Le téléchargement nécessite un accès à la bibliothèque YouScribe

__
Tout savoir sur nos offres
__

Description

Journal of Automated Reasoning manuscript No.

(will be inserted by the editor)

A list-machine benchmark for mechanized metatheory

Andrew W. Appel Robert Dockins

Xavier Leroy

the date of receipt and acceptance should be inserted later

Abstract We propose a benchmark to compare theorem-proving systems on their

ability to express proofs of compiler correctness. In contrast to the rst 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 speci c 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.

Keywords Theorem proving proof assistants program proof compiler veri cation

typed machine language metatheory Coq Twelf

1 How to evaluate mechanized metatheories

The POPLmark challenge [4] aims to compare the usability of several automated proof

assistants for mechanizing the kind of programming-language proofs that might be

done by the author of a POPL paper. The statement of rationale by the POPLmark

team (as of 26 June 2009) is,

How close are we to a world in which mechanically veri ed software is com-

monplace? A world in which theorem proving technology is used routinely by

both software developers and programming language researchers alike? One cru-

cial step towards achieving these goals is mechanized reasoning about ...

(will be inserted by the editor)

A list-machine benchmark for mechanized metatheory

Andrew W. Appel Robert Dockins

Xavier Leroy

the date of receipt and acceptance should be inserted later

Abstract We propose a benchmark to compare theorem-proving systems on their

ability to express proofs of compiler correctness. In contrast to the rst 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 speci c 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.

Keywords Theorem proving proof assistants program proof compiler veri cation

typed machine language metatheory Coq Twelf

1 How to evaluate mechanized metatheories

The POPLmark challenge [4] aims to compare the usability of several automated proof

assistants for mechanizing the kind of programming-language proofs that might be

done by the author of a POPL paper. The statement of rationale by the POPLmark

team (as of 26 June 2009) is,

How close are we to a world in which mechanically veri ed software is com-

monplace? A world in which theorem proving technology is used routinely by

both software developers and programming language researchers alike? One cru-

cial step towards achieving these goals is mechanized reasoning about ...

Sujets

Informations

Publié par | Ernoi |

Nombre de visites sur la page | 40 |

Langue | English |

Signaler un problème