gpg -vv -r myid -e -a name, on Nostr: design of the POPLmark benchmark is guided by features common to reasoning about ...

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 simply typed lambda calculus 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.
007, the POPLmark challenge is composed of three parts. Part 1 concerns solely the types of System F<: (System F with subtyping), 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
#popl
wiki
Image via Harper's slides