bcp.bib

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

@misc{Pierce:LambdaTA,
  author = {Benjamin C. Pierce},
  title = {Lambda, The Ultimate {TA}: {U}sing a Proof Assistant to Teach 
                  Programming Language Foundations},
  note = {Keynote address at {\em International Conference on 
                  Functional Programming (ICFP)}},
  year = 2009,
  plclub = {Yes},
  month = sep,
  bcp = {Yes},
  keys = {poplmark},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/LambdaTA.pdf}
}

@misc{Pierce:LambdaTA-ITP,
  author = {Benjamin C. Pierce},
  title = {Proof Assistant
                  as Teaching Assistant: A View from the Trenches},
  note = {Keynote address at {\em International Conference 
                  on Interactive Theorem Proving (ITP)}},
  year = 2010,
  plclub = {Yes},
  month = jul,
  bcp = {Yes},
  keys = {poplmark},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/LambdaTA-ITP.pdf}
}

@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},
  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{{\'e}}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, 
                  {L}ambda, 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}
}

@book{Pierce:SFold,
  author = {Benjamin C. Pierce and Arthur Azevedo de Amorim 
                  and Chris Casinghino and Marco Gaboardi and
                  Michael Greenberg and C\v{a}t\v{a}lin Hri\c{t}cu 
                  and Vilhelm Sj\"{o}berg and Brent Yorgey},
  title = {Software Foundations},
  year = {2017},
  publisher = {Electronic textbook},
  plclub = {Yes},
  bcp = {Yes},
  keys = {poplmark,books},
  note = {Version 5.0.  \URL{http://www.cis.upenn.edu/~bcpierce/sf}},
  ebook = {http://www.cis.upenn.edu/~bcpierce/sf},
  japanese = {http://proofcafe.org/sf}
}

@book{Pierce:SF1,
  author = {Benjamin C. Pierce and Arthur Azevedo de Amorim 
                  and Chris Casinghino and Marco Gaboardi and
                  Michael Greenberg and C\v{a}t\v{a}lin Hri\c{t}cu 
                  and Vilhelm Sj\"{o}berg and Brent Yorgey},
  title = {Logical Foundations},
  series = {Software Foundations series, volume 1},
  month = may,
  year = {2018},
  publisher = {Electronic textbook},
  plclub = {Yes},
  bcp = {Yes},
  keys = {poplmark,books},
  note = {Version 5.5.  \URL{http://www.cis.upenn.edu/~bcpierce/sf}},
  ebook = {http://www.cis.upenn.edu/~bcpierce/sf},
  japanese = {http://proofcafe.org/sf}
}

@book{Pierce:SF2,
  author = {Benjamin C. Pierce and Arthur Azevedo de Amorim 
                  and Chris Casinghino and Marco Gaboardi and
                  Michael Greenberg and C\v{a}t\v{a}lin Hri\c{t}cu 
                  and Vilhelm Sj\"{o}berg and Andrew Tolmach
                  and Brent Yorgey},
  title = {Programming Language Foundations},
  series = {Software Foundations series, volume 2},
  month = may,
  year = {2018},
  publisher = {Electronic textbook},
  plclub = {Yes},
  bcp = {Yes},
  keys = {poplmark,books},
  note = {Version 5.5.  \URL{http://www.cis.upenn.edu/~bcpierce/sf}},
  ebook = {http://www.cis.upenn.edu/~bcpierce/sf},
  japanese = {http://proofcafe.org/sf}
}