Skip to main content
Mechanized Metatheory for the Masses: The POPLMARK Challenge
Departmental Papers (CIS)
  • Brian E Aydemir, University of Pennsylvania
  • Aaron Bohannon, University of Pennsylvania
  • Matthew Fairbairn, University of Cambridge
  • J. Nathan Foster, University of Pennsylvania
  • Benjamin C Pierce, University of Pennsylvania
  • Peter Sewell, University of Cambridge
  • Dimitrios Vytiniotis, University of Pennsylvania
  • Geoffrey Washburn, University of Pennsylvania
  • Stephanie C Weirich, University of Pennsylvania
  • Stephan A Zdancewic, University of Pennsylvania
Date of this Version
Document Type
Conference Paper
Postprint version. Published in Lecture Notes in Computer Science, Volume 3603, Theorem Proving in Higher Order Logics (TPHOLs 2005), pages 50-65.
Publisher URL:
How close are we to a world where every paper on programming languages is accompanied by an electronic appendix with machinechecked 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.
Citation Information
Brian E Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, et al.. "Mechanized Metatheory for the Masses: The POPLMARK Challenge" (2005)
Available at: