POPLmark challenge
In programming language theory, the POPLmark challenge (from "Principles of Programming Languages benchmark", formerly Mechanized Metatheory for the Masses!) (Aydemir, 2005) is a set of benchmarks designed to evaluate the state of automated reasoning (or mechanization) in the metatheory of programming languages, and to stimulate discussion and collaboration among a diverse cross section of the formal methods community. Very loosely speaking, the challenge is about measurement of how well programs may be proven to match a specification of how they are intended to behave (and the many complex issues that this involves). 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 Workshop on Mech
- Comment
- enIn programming language theory, the POPLmark challenge (from "Principles of Programming Languages benchmark", formerly Mechanized Metatheory for the Masses!) (Aydemir, 2005) is a set of benchmarks designed to evaluate the state of automated reasoning (or mechanization) in the metatheory of programming languages, and to stimulate discussion and collaboration among a diverse cross section of the formal methods community. Very loosely speaking, the challenge is about measurement of how well programs may be proven to match a specification of how they are intended to behave (and the many complex issues that this involves). 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 Workshop on Mech
- Has abstract
- enIn programming language theory, the POPLmark challenge (from "Principles of Programming Languages benchmark", formerly Mechanized Metatheory for the Masses!) (Aydemir, 2005) is a set of benchmarks designed to evaluate the state of automated reasoning (or mechanization) in the metatheory of programming languages, and to stimulate discussion and collaboration among a diverse cross section of the formal methods community. Very loosely speaking, the challenge is about measurement of how well programs may be proven to match a specification of how they are intended to behave (and the many complex issues that this involves). 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 Workshop on Mechanized Metatheory is the main meeting of researchers participating in the challenge. 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: BindingMost 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.InductionProperties such as subject reduction and strong normalisation often require complex induction arguments.ReuseFurthering 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.
- Hypernym
- Set
- Is primary topic of
- POPLmark challenge
- Label
- enPOPLmark challenge
- Link from a Wikipage to an external page
- abella.cs.umn.edu/
- homepages.inf.ed.ac.uk/jcheney/programs/aprolog/
- www.seas.upenn.edu/~plclub/poplmark/
- Link from a Wikipage to another Wikipage
- ATS (programming language)
- Automated reasoning
- Benchmarking
- Benjamin C. Pierce
- Category:Formal methods
- Category:Programming language theory
- Category:Unsolved problems in computer science
- Coq
- Expression problem
- Formal methods
- Isabelle theorem prover
- LNCS
- Mathematical induction
- Matita proof assistant
- Metatheory
- Name binding
- Operational semantics
- Pattern matching
- Peter Sewell
- POPL
- Programming language theory
- QED manifesto
- Record (computer science)
- Simply typed lambda calculus
- Stephanie Weirich
- Strong normalisation
- Subject reduction
- Subtyping
- System F
- System F-sub
- Transitive relation
- Twelf
- Type safety
- University of Pennsylvania
- SameAs
- 4skyt
- m.02q8g3v
- POPLmark challenge
- Q7120017
- Subject
- Category:Formal methods
- Category:Programming language theory
- Category:Unsolved problems in computer science
- WasDerivedFrom
- POPLmark challenge?oldid=1044010307&ns=0
- WikiPageLength
- 4339
- Wikipage page ID
- 10323007
- Wikipage revision ID
- 1044010307
- WikiPageUsesTemplate
- Template:As of
- Template:ISBN
- Template:More citations needed
- Template:Multiple issues
- Template:No footnotes
- Template:Update-section