A List-Machine Benchmark for Mechanized Metatheory

被引：5

作者：

Appel, Andrew W. ^{[2
]}

Dockins, Robert ^{[2
]}

Leroy, Xavier ^{[1
]}

机构：

[1] INRIA Paris Rocquencourt, F-78153 Le Chesnay, France

[2] Princeton Univ, Princeton, NJ 08540 USA

来源：

JOURNAL OF AUTOMATED REASONING | 2012年 / 49卷 / 03期

关键词：

Theorem proving; Proof assistants; Program proof; Compiler verification; Typed machine language; Metatheory; Coq; Twelf; COMPILER;

D O I：

10.1007/s10817-011-9226-1

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

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.

引用

页码：453 / 491

页数：39

共 18 条

[1] [Anonymous], 5 ACM SIGPLAN INT C
[2] Appel Andrew W., 2007, POPL 2007. The 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, P109, DOI 10.1145/1190216.1190235
[3] Appel A. W., 2006, LIST MACHINE EXERCIS
[4] APPEL AW, 2000, HINTS PROVING THEORE
[5] Aydemir BE, 2005, LECT NOTES COMPUT SC, V3603, P50
[6] Bertot Y., 2004, EATCS TEXTS THEORETI
[7] Defunctionalized interpreters for programming languages
Danvy, Olivier
[J]. ACM SIGPLAN NOTICES, 2008, 43 (09) : 131 - 142
[8] Delahaye D, 2007, LECT NOTES COMPUT SC, V4732, P70
[9] A machine-checked model for a java']java-like language, virtual machine, and compiler
Klein, Gerwin
Nipkow, Tobias
[J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2006, 28 (04): : 619 - 695
[10] Towards the formal verification of a C0 compiler: Code generation and implementation correctness
Leinenbach, D
Paul, W
Petrova, E
[J]. SEFM 2005: THIRD IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS, 2005, : 2 - 11

← 1 2 →