The POPLmark Challenge

(via TYPES)

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!

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Thread tie-in

The section on representing binders (2.3) ties in nicely to the paper and thread here.