In programming language theory, the POPLmark challenge (formerly Mechanized Metatheory for the Masses!) is a set of benchmarks designed to evaluate the state of mechanization in the metatheory of programming languages, and to stimulate discussion and collaboration among a diverse cross section of the formal methods community. The challenge was initially proposed by the members of the PL club at the University of Pennsylvania, in association with collaborators around the world. The Workshop on Mechanized Metatheory is the main meeting of researchers participating in the challenge.
The design of the POPLmark benchmark is guided by features common to reasoning about programming languages. The challenge problems do not require the formalisation of large programming languages, but they do require sophistication in reasoning about:
- Binding
- Most programming languages have some form of binding, ranging in complexity from the simple binders of simply typed lambda calculus to complex, potentially infinite binders needed in the treatment of record patterns.
- Induction
- Properties such as subject reduction and strong normalisation often require complex induction arguments.
- Reuse
- Furthering collaboration being a key aim of the challenge, the solutions are expected to contain reusable components that would allow researchers to share language features and designs without requiring them to start from scratch every time.
Read more about POPLmark Challenge: The Problems, See Also
Famous quotes containing the word challenge:
“I don’t have any problem with a reporter or a news person who says the President is uninformed on this issue or that issue. I don’t think any of us would challenge that. I do have a problem with the singular focus on this, as if that’s the only standard by which we ought to judge a president. What we learned in the last administration was how little having an encyclopedic grasp of all the facts has to do with governing.”
—David R. Gergen (b. 1942)