A List-Machine Benchmark for Mechanized Metatheory
Journal of Automated Reasoning(2011)
摘要
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.
更多查看译文
关键词
Theorem proving,Proof assistants,Program proof,Compiler verification,Typed machine language,Metatheory,Coq,Twelf
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络