POPLmark challenge
In programming language theory, the POPLmark challenge (from "Principles of Programming Languages benchmark", formerly Mechanized Metatheory for the Masses!) (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. The challenge problems do not require the formalisation of large programming languages, but they do require sophistication in reasoning about: The problems. , the POPLmark challenge is composed of three parts. Part 1 concerns solely the types of System F (System F with subtyping), and has problems such as: Part 2 concerns  the syntax and semantics of System F. It concerns proofs of Part 3 concerns the usability of the formalisation of System F. In particular, the challenge asks for: Several solutions have been proposed for parts of the POPLmark challenge, using following tools: Isabelle/HOL, Twelf, Coq, αProlog, ATS, Abella and Matita.