The POPLmark Challenge is a concrete set of benchmarks
intended both for measuring progress and for stimulating
discussion and collaboration in mechanizing the metatheory of
programming languages. Since work on the challenge problems has
died down, the POPLmark wiki has been replaced with this static
page recording the submitted solutions and the project's history.
To gauge progress in mechanizing programming language
metatheory, we have issued a set of challenge problems chosen to
exercise many aspects of programming languages that are known to
be difficult to formalize.
- A description of the challenge problems:
- A preliminary version of the F sub interpreter (written in
- A set of test terms for Challenge 3:
Many researchers have created solutions to the POPLmark
Challenge. The following individuals and groups have submitted
solutions that remain accessible as of April, 2012 (names link
to pages about their submissions):
Summary of the encoding techniques and tools used by the
mailing list is no longer very active, but you may still
subscribe or view its archives.
Workshop on Mechanizing Metatheory was held on on October 4,
2007, in conjunction
with ICFP 2007.
Workshop on Mechanizing Metatheory was held at ICFP 2006, on
from the workshop are available.
A "Progress on Poplmark" meeting was held on January 15th,
2006. Some of the people working actively on PoplMark gathered to
discuss the solutions submitted so far.
This project has been supported by the National Science
Foundation, grant 0551589.