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.

• A description of the challenge problems: [pdf] [ps]
• A preliminary version of the F sub interpreter (written in OCaml): [tar.gz]
• A set of test terms for Challenge 3: [zip]

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):

• Stehan Berghofer
• Arthur Charguéraud (de Bruijn indices)
• Arthur Charguéraud (locally nameless)
• Adam Chlipala
• Alberto Ciaffaglione and Ivan Scagnetto
• Group from CMU (Michael Ashley-Rollman, Karl Crary, and Robert Harper)
• Matthew Fairbairn
• Andrew Gacek
• Xavier Leroy
• André Hirschowitz and Marco Maggesi
• Wilmer Ricciotti
• Aaron Stump
• Christian Urban et al.
• Jérôme Vouillon
• Hongwei Xi

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
HOAS			CMU				Gacek
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.

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.

People

The POPLmark team is:

• University of Pennsylvania: Brian E. Aydemir, Aaron Bohannon, Nate Foster, Benjamin Pierce, Jeff Vaughan, Dimitris Vytiniotis, Geoff Washburn, Stephanie Weirich, Steve Zdancewic
• University of Cambridge: Matthew Fairbairn, Peter Sewell

Acknowledgement

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