This HTML5 document contains 81 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dctermshttp://purl.org/dc/terms/
yago-reshttp://yago-knowledge.org/resource/
dbohttp://dbpedia.org/ontology/
foafhttp://xmlns.com/foaf/0.1/
n12https://global.dbpedia.org/id/
yagohttp://dbpedia.org/class/yago/
dbthttp://dbpedia.org/resource/Template:
rdfshttp://www.w3.org/2000/01/rdf-schema#
n21http://homepages.inf.ed.ac.uk/jcheney/programs/aprolog/
freebasehttp://rdf.freebase.com/ns/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n20https://www.seas.upenn.edu/~plclub/poplmark/
owlhttp://www.w3.org/2002/07/owl#
wikipedia-enhttp://en.wikipedia.org/wiki/
dbphttp://dbpedia.org/property/
provhttp://www.w3.org/ns/prov#
dbchttp://dbpedia.org/resource/Category:
xsdhhttp://www.w3.org/2001/XMLSchema#
goldhttp://purl.org/linguistics/gold/
wikidatahttp://www.wikidata.org/entity/
dbrhttp://dbpedia.org/resource/
n17http://abella.cs.umn.edu/

Statements

Subject Item
dbr:Benjamin_C._Pierce
dbo:wikiPageWikiLink
dbr:POPLmark_challenge
Subject Item
dbr:POPLmark_challenge
rdf:type
yago:Problem114410605 yago:Know-how105616786 yago:WikicatFormalMethods yago:Method105660268 yago:Cognition100023271 yago:Attribute100024264 yago:WikicatUnsolvedProblemsInComputerScience yago:PsychologicalFeature100023100 yago:Condition113920835 yago:Difficulty114408086 yago:Abstraction100002137 yago:State100024720 yago:Ability105616246
rdfs:label
POPLmark challenge
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
dcterms:subject
dbc:Programming_language_theory dbc:Formal_methods dbc:Unsolved_problems_in_computer_science
dbo:wikiPageID
10323007
dbo:wikiPageRevisionID
1044010307
dbo:wikiPageWikiLink
dbr:Mathematical_induction dbc:Unsolved_problems_in_computer_science dbr:Strong_normalisation dbr:Subtyping dbr:Benjamin_C._Pierce dbr:Type_safety dbr:Matita_proof_assistant dbr:Operational_semantics dbr:POPL dbr:Isabelle_theorem_prover dbr:System_F-sub dbr:University_of_Pennsylvania dbr:Coq dbr:ATS_(programming_language) dbr:Name_binding dbr:Transitive_relation dbr:Simply_typed_lambda_calculus dbr:LNCS dbc:Programming_language_theory dbr:Programming_language_theory dbr:Pattern_matching dbr:Benchmarking dbc:Formal_methods dbr:Subject_reduction dbr:Automated_reasoning dbr:Peter_Sewell dbr:System_F dbr:Twelf dbr:Metatheory dbr:Stephanie_Weirich dbr:QED_manifesto dbr:Record_(computer_science) dbr:Expression_problem dbr:Formal_methods
dbo:wikiPageExternalLink
n17: n20: n21:
owl:sameAs
n12:4skyt wikidata:Q7120017 freebase:m.02q8g3v yago-res:POPLmark_challenge
dbp:wikiPageUsesTemplate
dbt:No_footnotes dbt:Multiple_issues dbt:As_of dbt:More_citations_needed dbt:ISBN dbt:Update-section
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.
gold:hypernym
dbr:Set
prov:wasDerivedFrom
wikipedia-en:POPLmark_challenge?oldid=1044010307&ns=0
dbo:wikiPageLength
4339
foaf:isPrimaryTopicOf
wikipedia-en:POPLmark_challenge
Subject Item
dbr:Symposium_on_Principles_of_Programming_Languages
dbo:wikiPageWikiLink
dbr:POPLmark_challenge
Subject Item
dbr:Expression_problem
dbo:wikiPageWikiLink
dbr:POPLmark_challenge
Subject Item
dbr:Stephanie_Weirich
dbo:wikiPageWikiLink
dbr:POPLmark_challenge
Subject Item
dbr:POPLMARK
dbo:wikiPageWikiLink
dbr:POPLmark_challenge
dbo:wikiPageRedirects
dbr:POPLmark_challenge
Subject Item
dbr:POPLmark
dbo:wikiPageWikiLink
dbr:POPLmark_challenge
dbo:wikiPageRedirects
dbr:POPLmark_challenge
Subject Item
wikipedia-en:POPLmark_challenge
foaf:primaryTopic
dbr:POPLmark_challenge