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.
Challenge Problems
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.
Submitted Solutions
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 available submissions:
Mailing list
The POPLmark mailing list is no longer very active, but you may still subscribe or view its archives.
Meetings
The 2nd Workshop on Mechanizing Metatheory was held on on October 4, 2007, in conjunction with ICFP 2007.
The 1st Workshop on Mechanizing Metatheory was held at ICFP 2006, on September 21, 2006. Slides 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.
Acknowledgement
This project has been supported by the National Science Foundation, grant 0551589.