Mechanized Metatheory for the Masses: The PoplMark Challenge Export

@incollection{citeulike:5920185, abstract = {How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machine-checked proofs? We propose an initial set of benchmarks for measuring progress in this area. Based on the metatheory of System F , a typed lambda-calculus with second-order polymorphism, subtyping, and records, these benchmarks embody many aspects of programming languages that are challenging to formalize: variable binding at both the term and type levels, syntactic forms with variable numbers of components (including binders), and proofs demanding complex induction principles. We hope that these benchmarks will help clarify the current state of the art, provide a basis for comparing competing technologies, and motivate further research.}, author = {Aydemir, Brian E. and Bohannon, Aaron and Fairbairn, Matthew and Foster, J. Nathan and Pierce, Benjamin C. and Sewell, Peter and Vytiniotis, Dimitrios and Washburn, Geoffrey and Weirich, Stephanie and Zdancewic, Steve}, citeulike-article-id = {5920185}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/11541868_4}, citeulike-linkout-1 = {http://www.springerlink.com/content/7xd1vreytx2mjenc}, doi = {10.1007/11541868_4}, journal = {Theorem Proving in Higher Order Logics}, keywords = {coq, evaluation-contexts, isabelle, logical-frameworks, metatheory, theorem-proving, twelf}, pages = {50--65}, posted-at = {2009-10-10 21:17:21}, priority = {0}, title = {Mechanized Metatheory for the Masses: The PoplMark Challenge}, url = {http://dx.doi.org/10.1007/11541868_4}, year = {2005} }

TY - CHAP ID - citeulike:5920185 L3 - citeulike-article-id:5920185 N2 - How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machine-checked proofs? We propose an initial set of benchmarks for measuring progress in this area. Based on the metatheory of System F , a typed lambda-calculus with second-order polymorphism, subtyping, and records, these benchmarks embody many aspects of programming languages that are challenging to formalize: variable binding at both the term and type levels, syntactic forms with variable numbers of components (including binders), and proofs demanding complex induction principles. We hope that these benchmarks will help clarify the current state of the art, provide a basis for comparing competing technologies, and motivate further research. JF - Theorem Proving in Higher Order Logics EP - 65 TI - Mechanized Metatheory for the Masses: The PoplMark Challenge SP - 50 KW - coq KW - evaluation-contexts KW - isabelle KW - logical-frameworks KW - metatheory KW - theorem-proving KW - twelf AU - Aydemir, Brian AU - Bohannon, Aaron AU - Fairbairn, Matthew AU - Foster, Nathan AU - Pierce, Benjamin AU - Sewell, Peter AU - Vytiniotis, Dimitrios AU - Washburn, Geoffrey AU - Weirich, Stephanie AU - Zdancewic, Steve PY - 2005/// UR - http://dx.doi.org/10.1007/11541868_4 ER -