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:
“If combat means living in a ditch, females have biological problems staying in a ditch for 30 days because they get infections.... Males are biologically driven to go out and hunt giraffes.”
—Newt Gingrich (b. 1943)
“I believe that if we are to survive as a planet, we must teach this next generation to handle their own conflicts assertively and nonviolently. If in their early years our children learn to listen to all sides of the story, use their heads and then their mouths, and come up with a plan and share, then, when they become our leaders, and some of them will, they will have the tools to handle global problems and conflict.”
—Barbara Coloroso (20th century)