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}
}