[Our apologies for multiple copies.] The POPLmark Challenge How close are we to a world where programming language papers are routinely supported by machine-checked metatheory proofs, where full-scale language definitions are expressed in machine-processed mathematics, and where language implementations are directly tested against those definitions? To clarify the current state of the art, and to motivate further research, we propose some concrete benchmarks for measuring progress. Based on System Fsub, a typed lambda-calculus with second-order polymorphism, subtyping, and records, the benchmarks embody many aspects of programming languages that are challenging to formalize: variable binding at both the term and type levels, syntactic forms with variable numbers of components (including binders), proofs demanding complex induction principles, and algorithmic questions. To keep the challenge manageable, it is intermediate in scale between `toy' calculi and full programming languages. The challenge problems are available from the web page <http://www.cis.upenn.edu/group/proj/plclub/mmm/>, with informal definitions of syntax and semantics, hand proofs of the metatheoretic results, and a prototype implementation. We encourage users and developers of automated reasoning tools to attempt the challenges and send the results to the POPLmark mailing list (from that same web page), which will provide a forum for debate. Queries and clarifications should also be discussed there. The POPLmark team can also be mailed directly at provers@lists.seas.upenn.edu. We are not ourselves automated reasoning experts but rather potential users; our impression is that current tools are _almost_ at the point where they can be used routinely. It's time to bring mechanized metatheory to the masses - go to it! Peter, for the POPLmark team: Brian Aydemir, Aaron Bohannon, Matthew Fairbairn, Nathan Foster, Benjamin Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic