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:
“Our [adult] children have an adult’s right to make their own choices and have the responsibility of living with the consequences. If we make their problems ours, they avoid that responsibility, and we are faced with problems we can’t and shouldn’t solve.”
—Jane Adams (20th century)
“It’s so easy during those first few months to think that the problems will never end. You feel as if your son will never sleep through the night, will always spit up food after eating, and will never learn to smile—even though you don’t know any adults or even older children who still act this way.”
—Lawrence Kutner (20th century)