@comment{{This file has been generated by bib2bib 1.99}}
@comment{{Command line: bibtex2html-1.99-with-magiclink/bib2bib -c topic:"poplmark" -ob topic.poplmark.bib sewellbib2.bib}}
  author = {Brian E. Aydemir and Aaron Bohannon and Matthew Fairbairn
                  and J. Nathan Foster and Benjamin C. Pierce and Peter
                  Sewell and Dimitrios Vytiniotis and Geoffrey Washburn and
                  Stephanie Weirich and Steve Zdancewic},
  title = {Mechanized metatheory for the masses: {T}he {POPL}mark
  year = 2005,
  month = aug,
  optcrossref = {},
  optkey = {},
  conf = {TPHOLs 2005},
  booktitle = {Proceedings of  the 18th International Conference on Theorem Proving in Higher Order Logics (Oxford), LNCS 3603},
  pages = {50--65},
  optyear = {},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  optaddress = {},
  optmonth = {},
  optorganization = {},
  optpublisher = {},
  note = {},
  optannote = {},
  optpdf = {},
  project = {},
  url = {},
  doi = {10.1007/11541868_4},
  pdf = {},
  ps = {},
  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.
  topic = {poplmark}
  author = {Benjamin C. Pierce and Peter Sewell and
                   Stephanie Weirich and Steve Zdancewic},
  title = {It is Time to Mechanize Programming
                 Language Metatheory},
  conf = {VSTTE 2005},
  booktitle = {Verified Software: Theories, Tools, Experiments (Z\"urich)},
  year = 2005,
  optaddress = {, Switzerland},
  month = oct,
  note = {5pp},
  url = {},
  doi = {10.1007/978-3-540-69149-5_3},
  pdf = {},
  abstract = {How close are we to a world in which mechanically verified
software is commonplace? A world in which theorem proving technology
is used routinely by both software developers and programming language
researchers alike? One crucial step towards achieving these goals is mechanized
reasoning about language metatheory. The time has come to bring
together the theorem proving and programming language communities
to address this problem. We have proposed the POPLMark challenge
as a concrete set of benchmarks intended both for measuring progress in
this area and for stimulating discussion and collaboration. Our goal is
to push the boundaries of existing technology to the point where we can
achieve mechanized metatheory for the masses.},
  topic = {poplmark},
  project = {}