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. © IFIP International Federation for Information Processing 2008.
Cite
CITATION STYLE
Pierce, B. C., Sewell, P., Weirich, S., & Zdancewic, S. (2008). It is time to mechanize programming language metatheory. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4171 LNCS, pp. 26–30). https://doi.org/10.1007/978-3-540-69149-5_3
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
