About: POPLmark challenge

An Entity of Type: Abstraction100002137, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

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

Property	Value
dbo:abstract	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 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. (en)
dbo:wikiPageExternalLink	http://abella.cs.umn.edu/ http://homepages.inf.ed.ac.uk/jcheney/programs/aprolog/ https://www.seas.upenn.edu/~plclub/poplmark/
dbo:wikiPageID	10323007 (xsd:integer)
dbo:wikiPageLength	4339 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID	1044010307 (xsd:integer)
dbo:wikiPageWikiLink	dbr:Benchmarking dbr:Benjamin_C._Pierce dbr:Metatheory dbr:Peter_Sewell dbr:University_of_Pennsylvania dbr:Coq dbr:Mathematical_induction dbr:Operational_semantics dbr:Simply_typed_lambda_calculus dbr:Programming_language_theory dbr:Transitive_relation dbr:System_F-sub dbr:ATS_(programming_language) dbc:Unsolved_problems_in_computer_science dbr:Formal_methods dbr:QED_manifesto dbr:Record_(computer_science) dbr:Subject_reduction dbr:Twelf dbc:Formal_methods dbc:Programming_language_theory dbr:LNCS dbr:System_F dbr:Automated_reasoning dbr:Name_binding dbr:Pattern_matching dbr:Type_safety dbr:Expression_problem dbr:Subtyping dbr:Isabelle_theorem_prover dbr:POPL dbr:Stephanie_Weirich dbr:Strong_normalisation dbr:Matita_proof_assistant
dbp:wikiPageUsesTemplate	dbt:As_of dbt:ISBN dbt:More_citations_needed dbt:Multiple_issues dbt:No_footnotes dbt:Update-section
dcterms:subject	dbc:Unsolved_problems_in_computer_science dbc:Formal_methods dbc:Programming_language_theory
gold:hypernym	dbr:Set
rdf:type	yago:WikicatUnsolvedProblemsInComputerScience yago:Ability105616246 yago:Abstraction100002137 yago:Attribute100024264 yago:Cognition100023271 yago:Condition113920835 yago:Difficulty114408086 yago:Know-how105616786 yago:Method105660268 yago:Problem114410605 yago:PsychologicalFeature100023100 yago:State100024720 yago:WikicatFormalMethods
rdfs:comment	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 (en)
rdfs:label	POPLmark challenge (en)
owl:sameAs	freebase:POPLmark challenge yago-res:POPLmark challenge wikidata:POPLmark challenge https://global.dbpedia.org/id/4skyt
prov:wasDerivedFrom	wikipedia-en:POPLmark_challenge?oldid=1044010307&ns=0
foaf:isPrimaryTopicOf	wikipedia-en:POPLmark_challenge
is dbo:wikiPageRedirects of	dbr:POPLMARK dbr:POPLmark
is dbo:wikiPageWikiLink of	dbr:Benjamin_C._Pierce dbr:Symposium_on_Principles_of_Programming_Languages dbr:Expression_problem dbr:Stephanie_Weirich dbr:POPLMARK dbr:POPLmark
is foaf:primaryTopic of	wikipedia-en:POPLmark_challenge

This content was extracted from Wikipedia and is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License