Lambda the Ultimate

How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machine-checked proofs? To gauge progress in this area, we issue here a set of challenge problems, dubbed the POPLmark Challenge, chosen to exercise many aspects of programming languages that are known to be difficult to formalize.

A valid solution to the challenge will consist of appropriate software tools, a language representation strategy, and a demonstration that this infrastructure is sufficient to formalize the challenge problems.

The POPLmark team explains,

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!