POPLmark challenge

<h2 id="the-problems">The problems</h2>

<p>As of 2007<a href="https://en.wikipedia.org/w/index.php?title=POPLmark_challenge&action=edit">[update]</a>, the POPLmark challenge is composed of three parts. Part 1 concerns solely the types of <a href="/facts/System_F-sub/sJ73ej8w">System F<:</a> (<a href="/facts/System_F/odpwVpAG">System F</a> with <a href="/facts/Subtyping/0L9t8twv">subtyping</a>), and has problems such as:
</p>
<ol><li>Checking that the type system admits <a href="/facts/Transitive_relation/9r90y50r">transitivity</a> of subtyping.</li>
<li>Checking the transitivity of subtyping in the presence of <a href="/facts/Record_(computer_science)/1fvSgenB">records</a></li></ol>
<p>Part 2 concerns the syntax and semantics of System F<:. It concerns proofs of
</p>
<ol><li><a href="/facts/Type_safety/WxmEKq8R">Type safety</a> for the pure fragment</li>
<li>Type safety in the presence of <a href="/facts/Pattern_matching/CEwptMs9">pattern matching</a></li></ol>
<p>Part 3 concerns the usability of the formalisation of System F<:. In particular, the challenge asks for:
</p>
<ol><li>Simulating and animating the <a href="/facts/Operational_semantics/G24LXz6e">operational semantics</a></li>
<li>Extracting useful algorithms from the formalisations</li></ol>
<p>Several solutions have been proposed for parts of the POPLmark challenge, using following tools: <a href="/facts/Isabelle_theorem_prover/CNbtbX83">Isabelle/HOL</a>, <a href="/facts/Twelf/s6sIyor7">Twelf</a>, <a href="/facts/Coq_(software)/7oBXgLCE">Coq</a>, <a href="http://homepages.inf.ed.ac.uk/jcheney/programs/aprolog/">αProlog</a>, <a href="/facts/ATS_(programming_language)/0xB1ggUw">ATS</a>, <a href="http://abella.cs.umn.edu/">Abella</a> and <a href="/facts/Matita_proof_assistant/alTr7DnA">Matita</a>.
</p>
<h2 id="see-also">See also</h2>
<ul><li><a href="/facts/Expression_problem/NHg1NxqM">Expression problem</a></li>
<li><a href="/facts/QED_manifesto/jhWAuaGJ">QED manifesto</a></li>
<li><a href="/facts/POPL/kS3uDAkn">POPL</a> conference</li></ul>

<ul><li>Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, <a href="/facts/Benjamin_C._Pierce/m9DKUgML">Benjamin C. Pierce</a>, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, <a href="/facts/Stephanie_Weirich/0dtpKean">Stephanie C. Weirich</a>, and Stephan A. Zdancewic. Mechanized metatheory for the masses: The POPLmark challenge. In Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, volume 3603 of Lecture Notes in Computer Science, pages 50–65. Springer, Berlin/ Heidelberg/ New York, 2005.</li>
<li><a href="/facts/Benjamin_C._Pierce/m9DKUgML">Benjamin C. Pierce</a>, Peter Sewell, <a href="/facts/Stephanie_Weirich/0dtpKean">Stephanie Weirich</a>, Steve Zdancewic, <i>It Is Time to Mechanize Programming Language Metatheory</i>, In Bertrand Meyer, Jim Woodcock (Eds.) <i>Verified Software: Theories, Tools, Experiments</i>, <a href="/facts/LNCS/1UeA77BC">LNCS</a> 4171, Springer Berlin / Heidelberg, 2008, pp. 26–30, <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 978-3-540-69147-1</li></ul>
<h2 id="external-links">External links</h2>
<ul><li><a href="https://www.seas.upenn.edu/~plclub/poplmark/">The POPLmark Challenge</a></li></ul>

POPLmark challenge open-in-new

POPLmark challenge