It Is Time to Mechanize Programming Language Metatheory

How close are we to a world in which mechanically verified software is commonplace? A world in which theorem proving technology is used routinely by both software developers and programming language researchers alike? One crucial step towards achieving these goals is mechanized reasoning about language metatheory. The time has come to bring together the theorem proving and programming language communities to address this problem. We have proposed the POPLMark challenge as a concrete set of benchmarks intended both for measuring progress in this area and for stimulating discussion and collaboration. Our goal is to push the boundaries of existing technology to the point where we can achieve mechanized metatheory for the masses. 1 Mechanized Metatheory for the Masses One significant obstacle to achieving the goal of verified software is reasoning about the languages in which the software is written. Without formal models of programming languages, it is impossible to even state, let alo...

• Type: Conference
• Year: 2005
• Where: VSTTE
• Authors: Benjamin C. Pierce, Peter Sewell, Stephanie Weirich, Steve Zdancewic
• Keywords: Mechanized Metatheory, Programming Languages, Software Engineering, Theorem Proving, VSTTE 2005