bcp.bib

@PREAMBLE{{\newcommand{\SortNoop}[1]{}}}

@INPROCEEDINGS{poplmark,
  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 {POPLmark}
                  Challenge},
  booktitle = {International Conference on Theorem Proving in 
                  Higher Order Logics (TPHOLs)},
  year = 2005,
  month = {August},
  ps = {http://www.cis.upenn.edu/~geoffw/research/papers/poplmark.ps},
  psgz = {http://www.cis.upenn.edu/~geoffw/research/papers/poplmark.ps.gz},
  pdf = {http://www.cis.upenn.edu/~geoffw/research/papers/poplmark.pdf},
  plclub = {Yes},
  bcp = {Yes},
  keys = {poplmark},
  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 a concrete set of benchmarks for measuring
                  progress in this area. Based on the metatheory of System
                  F-sub, 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.}
}

@INPROCEEDINGS{Aydemir08,
  author = {Brian Aydemir and Arthur Chargu\'{e}raud and Benjamin C. Pierce and Randy Pollack and Stephanie Weirich},
  title = {Engineering formal metatheory},
  year = {2008},
  pages = {3--15},
  publisher = {ACM},
  booktitle = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
                     {L}anguages ({POPL}), San Francisco, California},
  year = {2008},
  month = JAN,
  bcp = {Yes},
  keys = {poplmark},
  plclub = {Yes},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/binders.pdf}
}

@MISC{Aydemir07a:old,
  author = {Brian Aydemir and Arthur Chargu{��}raud and Benjamin C. Pierce 
                  and Randy Pollack and Stephanie Weirich},
  title = {Engineering Formal Metatheory},
  year = {2007},
  month = JUL,
  keys = {poplmark},
  note = {Submitted for publication},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/binders.pdf}
}

@MISC{Pierce08LambdaTA,
  author = {Benjamin C. Pierce},
  title = {Using a Proof Assistant to Teach Programming Language Foundations, or, 
                  Lambda, the Ultimate {TA}},
  year = {2008},
  month = APR,
  bcp = {Yes},
  keys = {poplmark},
  plclub = {Yes},
  note = {White paper},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/plcurriculum.pdf}
}