POPLmark challenge

In type theory and programming languages, the POPLmark challenge is a set of benchmarks designed to evaluate the state of mechanization in the metatheory of programming languages, and to stimulate discussion and collaboration among a diverse cross section of the formal methods community. The challenge was initially proposed by the members of the "PL club" at the University of Pennsylvania, in association with collaborators around the world.

The design of the POPLmark benchmark is guided by features common to reasoning about programming languages. The challenge problems do not require the formalisation of large programming languages, but they do require sophistication in reasoning about:

; Binding : Most programming languages have some form of binding, ranging in complexity from the simple binders of simple type theory to complex, potentially infinite binders needed in the treatment of record patterns.; Induction : Properties such as subject reduction and strong normalisation often require complex induction arguments.; Reuse : Furthering collaboration being a key aim of the challenge, the solutions are expected to contain reusable components that would allow researchers to share language features and designs without requiring them to start from scratch every time.

The problems

As of 2007, the POPLmark challenge is composed of three parts. Part 1 concerns solely the types of System F_<:, and has problems such as:
# Checking that the type system admits transitivity of subtyping.
# Checking the transitivity of subtyping in the presence of records

Part 2 concerns the syntax and semantics of System F_<:. It concerns proofs of
# Type safety for the pure fragment
# Type safety in the presence of pattern matching

Part 3 concerns the usability of the formalisation of System F_<:. In particular, the challenge asks for:
# Simulating and animating the operational semantics
# Extracting useful algorithms from the formalisations

Several solutions have been proposed for parts of the POPLmark challenge, using tools such as Isabelle/HOL, Twelf, Coq and Matita.

See also

* The Workshop on Mechanized Metatheory, the main meeting of researchers participating in the challenge
* System F, the type-theoretic framework used for most of the challenge problems

External links

* [http://fling-l.seas.upenn.edu/~plclub/cgi-bin/poplmark/index.php?title=The_POPLmark_Challenge The POPLmark wiki]