Mechanized Metatheory for the Masses: The PoplMark Challenge
By Brian E. Aydemir, A. Bohannon, M. Fairbairn, Nate Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, Steve Zdancewic. International Conference on Theorem Proving in Higher Order Logics, 2005
374 citations recorded by the source corpus.
Subfields: Artificial Intelligence, Computational Theory and Mathematics
View Paper: https://www.semanticscholar.org/paper/89f4dc716039b7c4e52e9d34a074bf0dea488985
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Artificial Intelligence
- Jeremy G. Siek
- Walid Taha
- Christian Urban
- Michael Norrish
- Magnus O. Myreen
- Scott Owens
- Ramana Kumar
- Matteo Cimini
In Computational Theory and Mathematics
- Jeremy G. Siek
- Walid Taha
- Christian Urban
- Michael Norrish
- Magnus O. Myreen
- Scott Owens
- Ramana Kumar
- Matteo Cimini
Citations in the corpus
- Gradual Typing for Objects (2007, methodology): “Following the related work we give a programmer’s tour of gradual typing (Section 3) and an implementor’s tour of gradual typing (Section 4).”
- CakeML: a verified implementation of ML (2014, background): “, POPLMark [2]), but it has not typically focussed on fitting into the overall context of a verified compiler.”
- Nominal Techniques in Isabelle/HOL (2005, background): “The paper [4], which sets out some challenges for automated p roof assistants, claims that theorem proving technologies have almost reached the thres hold where they can be used by the massesfor formal reasoning about programming languages.”