The Problems
As of 2007, 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
Several solutions have been proposed for parts of the POPLmark challenge, using following tools: Isabelle/HOL, Twelf, Coq, αProlog, ATS, Abella and Matita.
Read more about this topic: POPLmark Challenge
Famous quotes containing the word problems:
“Nothing in the world can take the place of Persistence. Talent will not; nothing is more common than unsuccessful men with talent. Genius will not; unrewarded genius is almost a proverb. Education will not; the world is full of educated derelicts. Persistence and Determination alone are omnipotent. The slogan “Press On”, has solved and will always solve the problems of the human race.”
—Calvin Coolidge (1872–1933)
“There is an enormous chasm between the relatively rich and powerful people who make decisions in government, business, and finance and our poorer neighbors who must depend on these decisions to alleviate the problems caused by their lack of power and influence.”
—Jimmy Carter (James Earl Carter, Jr.)