(Aydemir, 2005) is a set of benchmarks designed to evaluate the state of automated reasoning (or mechanization) in the metatheory of programming languages, and to stimulate discussion and collaboration among a diverse cross section of the formal methods community.
Very loosely speaking, the challenge is about measurement of how well programs may be proven to match a specification of how they are intended to behave (and the many complex issues that this involves).
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.