1. It Is Time to Mechanize Programming Language Metatheory
- Author
-
Benjamin C. Pierce, Stephanie Weirich, Peter Sewell, and Steve Zdancewic
- Subjects
business.industry ,Programming language ,Computer science ,Proof assistant ,computer.software_genre ,Very high-level programming language ,Set (abstract data type) ,Automated theorem proving ,Software ,Metatheory ,POPLmark challenge ,business ,First-generation programming language ,computer - Abstract
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.
- Published
- 2008