[TYPES] The POPLmark Challenge

[Peter Sewell]

[Our apologies for multiple copies.]



                    The POPLmark Challenge

How close are we to a world where programming language papers are
routinely supported by machine-checked metatheory proofs, where
full-scale language definitions are expressed in machine-processed
mathematics, and where language implementations are directly tested
against those definitions?

To clarify the current state of the art, and to motivate further
research, we propose some concrete benchmarks for measuring progress.
Based on System Fsub, a typed lambda-calculus with second-order
polymorphism, subtyping, and records, the benchmarks embody many
aspects of programming languages that are challenging to formalize:
variable binding at both the term and type levels, syntactic forms
with variable numbers of components (including binders), proofs
demanding complex induction principles, and algorithmic questions.  
To keep the challenge manageable, it is intermediate in scale between
`toy' calculi and full programming languages.

The challenge problems are available from the web page

  <http://www.cis.upenn.edu/group/proj/plclub/mmm/>,

with informal definitions of syntax and semantics, hand proofs of the
metatheoretic results, and a prototype implementation. 

We encourage users and developers of automated reasoning tools to
attempt the challenges and send the results to the POPLmark mailing
list (from that same web page), which will provide a forum for debate.
Queries and clarifications should also be discussed there.  The
POPLmark team can also be mailed directly at provers at lists.seas.upenn.edu.

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!


Peter, for the POPLmark team:

  Brian Aydemir, Aaron Bohannon, Matthew Fairbairn, Nathan Foster,
  Benjamin Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey
  Washburn, Stephanie Weirich, and Steve Zdancewic