@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:SF, 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} }