About: POPLmark challenge

Facets (new session)
Description
Metadata
Settings
- Rule:
- Inverse Functional Properties:
- "Same As":

About: POPLmark challenge Goto Sponge NotDistinct Permalink

An Entity of Type : yago:WikicatFormalMethods, within Data Space : dbpedia.org associated with source document(s)
QRcode icon

http://dbpedia.org/describe/?url=http%3A%2F%2Fdbpedia.org%2Fresource%2FPOPLmark_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

Attributes	Values
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:label	POPLmark challenge (en)
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)
dcterms:subject	Unsolved problems in computer science Formal methods Programming language theory
Wikipage page ID	10323007 (xsd:integer)
Wikipage revision ID	1044010307 (xsd:integer)
Link from a Wikipage to another Wikipage	Benchmarking Benjamin C. Pierce Metatheory dbr:Peter_Sewell University of Pennsylvania Coq Mathematical induction Operational semantics Simply typed lambda calculus Programming language theory Transitive relation System F-sub ATS (programming language) Unsolved problems in computer science Formal methods QED manifesto Record (computer science) Subject reduction Twelf Formal methods Programming language theory LNCS System F Automated reasoning Name binding Pattern matching Type safety Expression problem Subtyping Isabelle theorem prover POPL Stephanie Weirich Strong normalisation Matita proof assistant
Link from a Wikipage to an external page	http://abella.cs.umn.edu/ http://homepages.inf.ed.ac.uk/jcheney/programs/aprolog/ https://www.seas.upenn.edu/~plclub/poplmark/
sameAs	POPLmark challenge POPLmark challenge POPLmark challenge POPLmark challenge
dbp:wikiPageUsesTemplate	dbt:As_of dbt:ISBN dbt:More_citations_needed dbt:Multiple_issues dbt:No_footnotes dbt:Update-section
has 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)
gold:hypernym	Set
prov:wasDerivedFrom	wikipedia-en:POPLmark_challenge?oldid=1044010307&ns=0
page length (characters) of wiki page	4339 (xsd:nonNegativeInteger)
foaf:isPrimaryTopicOf	wikipedia-en:POPLmark_challenge
is Link from a Wikipage to another Wikipage of	Benjamin C. Pierce Symposium on Principles of Programming Languages Expression problem Stephanie Weirich POPLMARK POPLmark
is Wikipage redirect of	POPLMARK POPLmark
is foaf:primaryTopic of	wikipedia-en:POPLmark_challenge

Faceted Search & Find service v1.17_git139 as of Feb 29 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 08.03.3330 as of Mar 19 2024, on Linux (x86_64-generic-linux-glibc212), Single-Server Edition (378 GB total memory, 54 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software