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:

Alpha Prolog Coq Twelf ATS Isabelle/HOL Matita Abella
de Bruijn Vouillon, Charguéraud (a) Berghofer
Weak HOAS Ciaffaglione and Scagnetto
Hybrid Xi
Locally nameless Chlipala, Leroy, Charguéraud (b) Ricciotti
Named variables Stump
Nested abstract syntax Hirschowitz and Maggesi
Nominal Fairbairn Urban et al.

Mailing list

The POPLmark mailing list is no longer very active, but you may still subscribe or view its archives.


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.


The POPLmark team is:


This project has been supported by the National Science Foundation, grant 0551589.