bcp.bib

@preamble{{\newcommand{\SortNoop}[1]{}}}
@misc{Pierce:gridapple,
  author = {Benjamin C. Pierce},
  title = {{\sc Gridapple}: an implementation of the {\sc ESRI} {\sc
                  Grid} system for the {Apple-II}},
  year = {1981},
  note = {Marketed by Environmental Systems Research Institute,
                  Redlands, CA},
  plclub = {Yes},
  bcp = {Yes}
}
@inproceedings{Pierce82,
  author = {B. C. Pierce},
  title = {A Microcomputer-Based Geographic Information System},
  booktitle = {Proceedings of the Seventh West Coast Computer Faire},
  month = mar,
  year = 1982,
  plclub = {Yes},
  bcp = {Yes}
}
@misc{Larrabee&82,
  author = {T. Larrabee and K. McCall and C. Mitchell and B. C.
                  Pierce},
  title = {Gambit: {A} Video Game Programming Language},
  howpublished = {Project report for Stanford CS-242 (Programming Language
                  Design)},
  month = {December},
  year = 1982,
  note = {See also: Larrabee, T. and Mitchell, C. ``Gambit: A
                  Prototyping Approach to Video Game Design.'' IEEE Software,
                  Vol. 1 No. 4, Oct. 1984.},
  plclub = {Yes},
  bcp = {Yes}
}
@inproceedings{Pierce84,
  author = {B. C. Pierce},
  title = {Gridapple: {A} Microcomputer-Based Geographic Information
                  System},
  booktitle = {Harvard Computer Graphics Week},
  month = jul,
  year = 1982,
  note = {Reprinted in Marble, D., et al, {\em Basic Readings in
                  Geographic Information Systems.} Williamsville, NY: SPAD
                  Systems, Ltd., 1984},
  plclub = {Yes},
  bcp = {Yes}
}
@misc{Pierce:arcinfo,
  author = {Benjamin C. Pierce},
  title = {{\sc Arc-Info} plotting and display subsystem},
  year = {1982},
  note = {Marketed by Environmental Systems Research Institute,
                  Redlands, CA, USA},
  plclub = {Yes},
  bcp = {Yes}
}
@misc{Pierce:artemis,
  author = {Benjamin C. Pierce},
  title = {{\sc Artemis}: a graphics editor for circuit diagrams},
  year = {1986},
  note = {Used internally at DEC Western Research Lab for the design
                  of the {\sc Titan} processor and power/packaging},
  plclub = {Yes},
  bcp = {Yes}
}
@techreport{Habermann&88,
  author = {A. N. Habermann and Charles Krueger and Benjamin Pierce
                  and Barbara Staudt and John Wenn},
  title = {Programming with Views},
  institution = {Carnegie Mellon University, Computer Science Department},
  number = {CMU-CS-87-177},
  month = jan,
  year = {1988},
  plclub = {Yes},
  bcp = {Yes}
}
@techreport{PIERCE89B,
  key = {Pierce89b},
  author = {Benjamin Pierce},
  title = {A Decision Procedure for the Subtype Relation on
                  Intersection Types with Bounded Variables},
  institution = {School of Computer Science, Carnegie Mellon University},
  type = {Technical Report},
  number = {CMU-CS-89-169},
  month = sep,
  year = {1989},
  plclub = {Yes},
  bcp = {Yes}
}
@unpublished{PIERCE89C,
  key = {PIERCE89C},
  author = {Benjamin Pierce},
  title = {Bounded Quantification and Intersection Types},
  month = sep,
  year = {1989},
  note = {Thesis proposal (unpublished)},
  plclub = {Yes},
  bcp = {Yes}
}
@techreport{PIERCE89,
  key = {Pierce89},
  author = {Benjamin Pierce and Scott Dietzen and Spiro Michaylov},
  title = {Programming in Higher-order Typed Lambda-Calculi},
  institution = {Carnegie Mellon University},
  type = {Technical Report},
  number = {CMU-CS-89-111},
  month = mar,
  year = {1989},
  plclub = {Yes},
  bcp = {Yes},
  tr = {http://www.cis.upenn.edu/~bcpierce/papers/leap.pdf},
  errata = {http://www.cis.upenn.edu/~bcpierce/papers/leap.errata},
  keys = {typessurveys}
}
@techreport{HarperPierce90,
  author = {Robert W. Harper and Benjamin C. Pierce},
  title = {Extensible Records Without Subsumption},
  institution = {School of Computer Science, Carnegie Mellon University},
  year = {1990},
  month = feb,
  type = {Technical Report},
  number = {CMU-CS-90-102},
  plclub = {Yes},
  bcp = {Yes}
}
@unpublished{Pierce90b,
  author = {Benjamin C. Pierce},
  title = {Preliminary Investigation of a Calculus with Intersection
                  and Union Types},
  year = 1990,
  month = jun,
  note = {Unpublished manuscript},
  plclub = {Yes},
  bcp = {Yes}
}
@inproceedings{HarperPierce91,
  author = {Robert Harper and Benjamin Pierce},
  title = {A Record Calculus Based on Symmetric Concatenation},
  booktitle = {{ACM} {S}ymposium on {P}rinciples of {P}rogramming
                     {L}anguages ({POPL}), Orlando, Florida},
  year = 1991,
  pages = {131--142},
  month = jan,
  note = {Extended version available as Carnegie Mellon Technical
                  Report CMU-CS-90-157},
  plclub = {Yes},
  bcp = {Yes}
}
@book{PIERCE91,
  author = {Benjamin C. Pierce},
  title = {Basic Category Theory for Computer Scientists},
  year = {1991},
  publisher = {MIT Press},
  fullisbn = {0-262-66071-7},
  orderinginfo = {MIT PRESS 55 Hayward ST. Cambridge Mass 02142 USA
                  800-356-0343},
  europeinfo = {14 Bloomsbury Square London WC1A 2LP U.K. Facsimile:
                  071-404-0601},
  plclub = {Yes},
  bcp = {Yes},
  keys = {books}
}
@article{ABADI91,
  author = {Mart\'{\i}n Abadi and Luca Cardelli and Benjamin Pierce
                  and Gordon Plotkin},
  title = {Dynamic Typing in a Statically Typed Language},
  journal = {ACM Transactions on Programming Languages and Systems},
  publisher = {ACM},
  year = 1991,
  volume = 13,
  number = 2,
  month = apr,
  pages = {237--268},
  note = {Summary in \bgroup\em {ACM} {S}ymposium on {P}rinciples of {P}rogramming
                     {L}anguages ({POPL}), Austin, Texas\egroup, 1989},
  plclub = {Yes},
  bcp = {Yes}
}
@article{ABADI91B,
  author = {Mart\'{\i}n Abadi and Benjamin Pierce and Gordon Plotkin},
  title = {Faithful Ideal Models for Recursive Polymorphic Types},
  journal = {International Journal of Foundations of Computer Science},
  volume = 2,
  number = 1,
  month = mar,
  year = 1991,
  pages = {1--21},
  note = {Summary in Fourth Annual Symposium on Logic in Computer
                  Science, June, 1989},
  plclub = {Yes},
  bcp = {Yes}
}
@techreport{Pierce91b,
  author = {Benjamin C. Pierce},
  title = {Programming with Intersection Types, Union Types, and
                  Polymorphism},
  institution = {Carnegie Mellon University},
  type = {Technical Report},
  number = {CMU-CS-91-106},
  month = feb,
  year = {1991},
  plclub = {Yes},
  bcp = {Yes}
}
@phdthesis{PierceThesis,
  author = {Benjamin C. Pierce},
  title = {Programming with Intersection Types and Bounded
                  Polymorphism},
  school = {Carnegie Mellon University},
  month = {December},
  year = {1991},
  note = {Available as School of Computer Science technical report
                  CMU-CS-91-205},
  ascii = {Benjamin C. Pierce, "Programming with Intersection Types
                  and Bounded Polymorphism." Ph.D. thesis, Carnegie Mellon
                  University, December, 1991. Available as School of Computer
                  Science technical report CMU-CS-91-205.},
  plclub = {Yes},
  bcp = {Yes}
}
@misc{Pierce:fmeet,
  author = {Benjamin C. Pierce},
  title = {{\sc Fmeet}: a polymorphic $\lambda$-calculus with
                  intersection types},
  year = {1991},
  plclub = {Yes},
  bcp = {Yes}
}
@techreport{HofmannPierce92:TR,
  author = {Martin Hofmann and Benjamin Pierce},
  title = {An Abstract View of Objects and Subtyping (Preliminary
                  Report)},
  institution = {University of Edinburgh, LFCS},
  type = {Technical Report},
  number = {ECS-LFCS-92-226},
  year = {1992},
  plclub = {Yes},
  bcp = {Yes}
}
@unpublished{Pierce92d,
  author = {Benjamin C. Pierce and Robert Pollack},
  title = {Higher-Order Subtyping},
  year = {1992},
  month = aug,
  note = {Unpublished manuscript},
  plclub = {Yes},
  bcp = {Yes}
}
@unpublished{Pierce:delegation,
  author = {Benjamin C. Pierce},
  title = {A Model of Delegation Based on Existential Types},
  year = {1993},
  month = apr,
  note = {Available electronically},
  plclub = {Yes},
  bcp = {Yes},
  keys = {oop},
  ps = {http://www.cis.upenn.edu/~bcpierce/papers/delegation.ps}
}
@misc{Pierce:Kyoto-talk,
  author = {Benjamin C. Pierce},
  title = {A Typed Higher-Order Programming Language Based on the
                  Pi-Calculus},
  month = jul,
  year = {1993},
  note = {Invited lecture at {\em Workshop on Type Theory and its
                  Application to Computer Systems}, Kyoto University},
  plclub = {Yes},
  bcp = {Yes}
}
@inproceedings{PierceRemyTurner93,
  author = {Benjamin C. Pierce and Didier R\'emy and David N. Turner},
  title = {A Typed Higher-Order Programming Language Based on the
                  Pi-Calculus},
  month = jul,
  year = {1993},
  booktitle = {Workshop on Type Theory and its Application to Computer
                  Systems, Kyoto University},
  plclub = {Yes},
  bcp = {Yes}
}
@unpublished{Pierce92g,
  author = {Benjamin C. Pierce},
  title = {F-Omega-Sub User's Manual, Version 1.4},
  year = {1993},
  month = feb,
  note = {Available by FTP as part of the {\tt fomega}
                  implementation},
  plclub = {Yes},
  bcp = {Yes}
}
@unpublished{Pierce:mutable,
  author = {Benjamin C. Pierce},
  title = {Mutable Objects},
  year = {1993},
  month = jun,
  note = {Draft report; available electronically},
  plclub = {Yes},
  bcp = {Yes},
  keys = {oop},
  ps = {http://www.cis.upenn.edu/~bcpierce/papers/mutable.ps}
}
@inproceedings{PierceTurner92:POPL,
  author = {Benjamin C. Pierce and David N. Turner},
  title = {Object-Oriented Programming Without Recursive Types},
  booktitle = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
                     {L}anguages ({POPL}), Charleston, South Carolina},
  year = {1993},
  month = jan,
  pages = {299--312},
  plclub = {Yes},
  bcp = {Yes}
}
@unpublished{Pierce93c,
  author = {Benjamin Pierce},
  title = {Object-Oriented Programming in Typed Lambda-Calculus:
                  Exercises and Solutions},
  year = {1993},
  month = apr,
  note = {Lecture notes for 1992 Frankische OOrientierungstage,
                  University of Erlangen, Germany (revised version)},
  plclub = {Yes},
  bcp = {Yes}
}
@techreport{PierceTurner92b,
  author = {Benjamin C. Pierce and David N. Turner},
  title = {Statically Typed Friendly Functions via Partially Abstract
                  Types},
  institution = {University of Edinburgh, LFCS},
  type = {Technical Report},
  number = {ECS-LFCS-93-256},
  month = apr,
  year = {1993},
  note = {Also available as INRIA-Rocquencourt Rapport de Recherche
                  No. 1899},
  plclub = {Yes},
  bcp = {Yes},
  keys = {oop},
  ps = {http://www.cis.upenn.edu/~bcpierce/papers/friendly.ps}
}
@misc{Pierce:JFLA-talk,
  author = {Benjamin C. Pierce},
  title = {Typage des Traits Orient\'es-Objets},
  month = feb,
  year = {1993},
  note = {Invited lecture at {\em Journe\'es Francophones des
                  Langages Applicatifs}, Annecy, France},
  plclub = {Yes},
  bcp = {Yes}
}
@inproceedings{PierceSangiorgi95,
  author = {Benjamin C. Pierce and Davide Sangiorgi},
  title = {Typing and Subtyping for Mobile Processes},
  booktitle = {Logic in Computer Science},
  year = {1993},
  note = {Full version in \bgroup\em Mathematical Structures in
                  Computer Science \egroup, Vol.\ 6, No.\ 5, 1996},
  full = {http://www.cis.upenn.edu/~bcpierce/papers/pi.ps},
  plclub = {Yes},
  bcp = {Yes},
  keys = {pict}
}
@misc{Pierce:fomega,
  author = {Benjamin C. Pierce},
  title = {{\sc F-Omega-Sub}: a polymorphic $\lambda$-calculus with
                  higher-order subtyping and object-oriented extensions},
  year = {1993},
  plclub = {Yes},
  bcp = {Yes}
}
@article{Pierce92a,
  author = {Benjamin C. Pierce},
  title = {Bounded Quantification is Undecidable},
  journal = {Information and Computation},
  year = 1994,
  volume = 112,
  number = 1,
  pages = {131--165},
  month = jul,
  note = {Also in C. A. Gunter and J. C. Mitchell, editors, {\em
                    Theoretical Aspects of Object-Oriented Programming:
                    Types, Semantics, and Language Design}, MIT Press, 1994. Summary in \bgroup \em {ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
                     {L}anguages ({POPL}), Albuquerque, New Mexico\egroup},
  plclub = {Yes},
  bcp = {Yes},
  keys = {subtyping},
  conf = {http://www.cis.upenn.edu/~bcpierce/papers/fsubpopl.ps}
}
@misc{Pierce:COPC-talk,
  author = {Benjamin C. Pierce},
  title = {Concurrent Objects in a Process Calculus},
  note = {Invited lecture at {\em Theory and Practice of Parallel
                  Programming (TPPP)}, Sendai, Japan},
  year = 1994,
  month = nov,
  plclub = {Yes},
  bcp = {Yes}
}
@inproceedings{CastagnaPierce93,
  author = {Giuseppe Castagna and Benjamin Pierce},
  title = {Decidable Bounded Quantification},
  booktitle = {Proceedings of the Twenty-First {ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
                     {L}anguages ({POPL}), Portland, Oregon},
  publisher = {ACM},
  year = 1994,
  month = jan,
  plclub = {Yes},
  bcp = {Yes},
  keys = {subtyping},
  ps = {http://www.cis.upenn.edu/~bcpierce/papers/fsubnew.ps}
}
@inproceedings{PierceSteffen95,
  author = {Benjamin C. Pierce and Martin Steffen},
  realauthor = {Benjamin Pierce and Martin Steffen},
  title = {Higher-Order Subtyping},
  booktitle = {IFIP Working Conference on Programming Concepts, Methods
                  and Calculi (PROCOMET)},
  year = 1994,
  note = {Full version in \bgroup\em Theoretical Computer
                  Science\egroup, vol.~176, no.~1--2, pp.\  235--282, 1997
                  (corrigendum in TCS vol.~184 (1997), p.~247)},
  plclub = {Yes},
  bcp = {Yes},
  keys = {subtyping},
  tr = {http://www.cis.upenn.edu/~bcpierce/papers/fomega.ps}
}
@techreport{SteffenPierce93:TR,
  author = {Martin Steffen and Benjamin Pierce},
  title = {Higher-Order Subtyping},
  year = {1994},
  month = jan,
  institution = {LFCS, University of Edinburgh},
  number = {ECS-LFCS-94-280},
  note = {Also available as {Universit\"at Erlangen-N\"urnberg
                  Interner Bericht IMMD7-01/94}. To appear in Theoretical
                  Computer Science.},
  plclub = {Yes},
  bcp = {Yes}
}
@techreport{HofmannPierce94a:TR,
  author = {Martin Hofmann and Benjamin Pierce},
  title = {Positive Subtyping},
  year = {1994},
  month = sep,
  institution = {LFCS, University of Edinburgh},
  number = {ECS-LFCS-94-303},
  plclub = {Yes},
  bcp = {Yes}
}
@article{PierceTurner92,
  author = {Benjamin C. Pierce and David N. Turner},
  title = {Simple Type-Theoretic Foundations for Object-Oriented
                  Programming},
  note = {Summary in \bgroup\em {ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
                     {L}anguages ({POPL}), Charleston, South Carolina\egroup, 1993},
  journal = {Journal of Functional Programming},
  volume = 4,
  number = 2,
  month = apr,
  pages = {207--247},
  year = {1994},
  plclub = {Yes},
  bcp = {Yes},
  pdf = {http://www.cis.upenn.edu/~bcpierce/papers/oop.pdf},
  ps = {http://www.cis.upenn.edu/~bcpierce/papers/oop.ps},
  conf = {http://www.cis.upenn.edu/~bcpierce/papers/oop-popl.ps},
  keys = {oop}
}
@article{Pierce94a,
  author = {Benjamin C. Pierce},
  title = {Woggles from {O}z: {W}riting Interactive Fiction},
  note = {Expanded version available electronically},
  journal = {Leonardo: Journal of the International Society for the
                  Arts, Sciences, and Technology},
  year = {1994},
  plclub = {Yes},
  bcp = {Yes}
}
@article{HofmannPierce94,
  author = {Martin Hofmann and Benjamin Pierce},
  title = {A Unifying Type-Theoretic Framework for Objects},
  journal = {Journal of Functional Programming},
  volume = {5},
  number = {4},
  pages = {593--635},
  month = oct,
  note = {Previous versions appeared in the Symposium on Theoretical
                  Aspects of Computer Science, 1994, (pages 251--262) and,
                  under the title ``An Abstract View of Objects and Subtyping
                  (Preliminary Report),'' as University of Edinburgh, LFCS
                  technical report ECS-LFCS-92-226, 1992},
  year = 1995,
  plclub = {Yes},
  bcp = {Yes},
  ps = {http://www.cis.upenn.edu/~bcpierce/papers/abstroop.ps},
  keys = {oop}
}
@inproceedings{PierceTurner94:COPC,
  author = {Benjamin C. Pierce and David N. Turner},
  title = {Concurrent Objects in a Process Calculus},
  booktitle = {Theory and Practice of Parallel Programming (TPPP),
                  Sendai, Japan (Nov.{} 1994)},
  editor = {Takayasu Ito and Akinori Yonezawa},
  year = {1995},
  month = apr,
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  number = {907},
  pages = {187--215},
  short = {``Concurrent Objects in a Process Calculus,'' Benjamin C.
                  Pierce and David N. Turner, invited lecture at {\it Theory
                  and Practice of Parallel Programming (TPPP)}, Sendai, Japan
                  (Nov.{} 1994). Springer Lecture Notes in Computer Science
                  907, pp.~187--215},
  plclub = {Yes},
  bcp = {Yes},
  keys = {pict},
  url = {http://www.cis.upenn.edu/~bcpierce/papers/copc.ps}
}
@inproceedings{CastagnaPierce95,
  author = {Giuseppe Castagna and Benjamin Pierce},
  title = {Corrigendum: Decidable Bounded Quantification},
  booktitle = {Proceedings of the Twenty-Second {ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
                     {L}anguages ({POPL}), Portland, Oregon},
  publisher = {ACM},
  year = 1995,
  month = jan,
  plclub = {Yes},
  bcp = {Yes},
  keys = {subtyping},
  ps = {http://www.cis.upenn.edu/~bcpierce/papers/fsubnew-corrigendum.ps}
}
@article{Abadi92,
  author = {Mart\'{\i}n Abadi and Luca Cardelli and Benjamin Pierce
                  and Didier R\'{e}my},
  title = {Dynamic Typing in Polymorphic Languages},
  journal = {Journal of Functional Programming},
  volume = {5},
  number = {1},
  pages = {111--130},
  month = jan,
  note = {Summary in \bgroup \em ACM SIGPLAN Workshop on ML and its
                  Applications\egroup, June 1992},
  year = 1995,
  plclub = {Yes},
  bcp = {Yes}
}
@misc{Pierce:LinearPiTalk,
  author = {Benjamin C. Pierce},
  title = {Linearity and the Pi-Calculus},
  note = {Invited lecture at {\em Advances in Type Systems for
                  Computation}, Cambridge, England},
  year = 1995,
  month = aug,
  plclub = {Yes},
  bcp = {Yes}
}
@misc{KobayashiPierceTurner:LinearPiTR,
  author = {Naoki Kobayashi and Benjamin C. Pierce and David N.
                  Turner},
  title = {Linearity and the Pi-Calculus},
  year = {1995},
  note = {Technical report, Department of Information Science,
                  University of Tokyo and Computer Laboratory, University of
                  Cambridge},
  plclub = {Yes},
  bcp = {Yes}
}
@inproceedings{HofmannPierce94a,
  author = {Martin Hofmann and Benjamin Pierce},
  title = {Positive Subtyping},
  booktitle = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
                     {L}anguages ({POPL}), San Francisco, California},
  year = {1995},
  month = jan,
  pages = {186--197},
  note = {Full version in \bgroup\em Information and
                  Computation\egroup, volume 126, number 1, April 1996. Also
                  available as University of Edinburgh technical report
                  ECS-LFCS-94-303, September 1994},
  plclub = {Yes},
  bcp = {Yes},
  keys = {oop},
  ps = {http://www.cis.upenn.edu/~bcpierce/papers/pos.ps}
}
@misc{Pierce:LICSSurvey,
  author = {Benjamin C. Pierce},
  title = {Types and Programming Languages: The Next Generation},
  note = {Invited tutorial at {\em Logic in Computer Science (LICS)}},
  year = 2003,
  plclub = {Yes},
  bcp = {Yes},
  keys = {typessurveys},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/tng-lics2003-slides.pdf}
}
@misc{Pierce:ICMTtalk,
  author = {Benjamin C. Pierce},
  title = {Foundations for Bidirectional Programming, or: {H}ow To Build
                  a Bidirectional Programming Language},
  note = {Keynote address at {\em International Conference
                  on Model Transformation (ICMT)}},
  year = 2009,
  month = jun,
  plclub = {Yes},
  bcp = {Yes},
  keys = {harmony},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/icmt-2009-slides.pdf}
}
@misc{Pierce:CERNtalk,
  author = {Benjamin C. Pierce},
  title = {Mysteries of Dropbox},
  note = {Keynote address at CERN {\em Workshop on Cloud Services for File Synchronisation and Sharing}},
  year = 2014,
  month = nov,
  plclub = {Yes},
  bcp = {Yes},
  keys = {harmony},
  slides = {https://indico.cern.ch/event/336753/session/1/contribution/28},
  video = {https://indico.cern.ch/event/336753/session/1/contribution/28}
}
@misc{Pierce:ClojureConjtalk,
  author = {Benjamin C. Pierce},
  title = {A Deep Specification for Dropbox},
  note = {Keynote address at Clojure/conj},
  year = 2015,
  month = nov,
  plclub = {Yes},
  bcp = {Yes},
  keys = {harmony},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/clojure-deepspec-2015.pdf},
  video = {https://www.youtube.com/watch?v=Y2jQe8DFzUM}
}
@inproceedings{MysteriesOfDropbox2016,
  author = {John Hughes and Benjamin C. Pierce and Thomas Arts
                  and Ulf Norell},
  title = {Mysteries of {D}ropbox: {P}roperty-Based Testing
                  of a Distributed
                  Synchronization Service},
  year = 2016,
  booktitle = {International Conference on Software Testing,
                  Verification and Validation (ICST)},
  month = apr,
  plclub = {Yes},
  bcp = {Yes},
  keys = {verification},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/ICST-2015-mysteries.pdf},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/mysteriesofdropbox.pdf}
}
@misc{Pierce:ChalmersDeepspecTalk,
  author = {Benjamin C. Pierce},
  title = {The Age of Deep Specification},
  note = {Honorary doctorate address at Chalmers University},
  year = 2015,
  month = may,
  plclub = {Yes},
  bcp = {Yes},
  akeys = {verification},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/chalmers-deepspec-2015.pdf}
}
@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 = {verification},
  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 = {verification},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/LambdaTA-ITP.pdf}
}
@misc{Pierce:ModulesTutorial,
  author = {Benjamin C. Pierce},
  title = {Advanced Module Systems: A Guide for the Perplexed},
  note = {Invited tutorial at {\em International Conference on Functional
                  Programming (ICFP)}},
  year = 2000,
  plclub = {Yes},
  bcp = {Yes},
  keys = {typessurveys},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/modules-icfp.ps}
}
@misc{Pierce:HorizonDayTalk,
  author = {Benjamin C. Pierce},
  title = {Using Types to Compare Objects and {ADT}s},
  note = {Invited lecture at {\em Horizon Day}, Indiana University},
  year = 1995,
  month = oct,
  plclub = {Yes},
  bcp = {Yes}
}
@inproceedings{BruceCardelliPierce96:old,
  author = {Kim B. Bruce and Luca Cardelli and Benjamin C. Pierce},
  title = {Comparing Object Encodings},
  booktitle = {Invited lecture at Third Workshop on Foundations of Object
                  Oriented Languages (FOOL 3)},
  year = 1996,
  month = jul,
  plclub = {Yes},
  bcp = {Yes}
}
@inproceedings{NestmannPierce96,
  author = {Uwe Nestmann and Benjamin C. Pierce},
  title = {Decoding Choice Encodings},
  booktitle = {Proceedings of CONCUR '96},
  year = 1996,
  month = aug,
  note = {Full version in \bgroup\em Information and
                  Computation\egroup, 163(1): 1--59 (2000)},
  plclub = {Yes},
  bcp = {Yes},
  full = {http://www.cis.upenn.edu/~bcpierce/papers/choice.ps},
  keys = {pict}
}
@unpublished{Pierce:EvenSimpler,
  author = {Benjamin C. Pierce},
  title = {Even simpler type-theoretic foundations for {OOP}},
  month = mar,
  year = {1996},
  note = {Manuscript (circulated electronically)},
  plclub = {Yes},
  bcp = {Yes}
}
@incollection{EncyOfDBs09,
  author = {V\'{e}ronique Benzaken and Giuseppe Castagna and Haruo
                  Hosoya and Benjamin C. Pierce and Stijn Vansummeren},
  title = {{XML}  Typechecking},
  booktitle = {Encyclopedia of Database Systems},
  publisher = {Springer},
  year = {2009},
  plclub = {Yes},
  bcp = {Yes},
  keys = {xduce}
}
@incollection{Pierce95a,
  author = {Benjamin C. Pierce},
  title = {Foundational Calculi for Programming Languages},
  booktitle = {Handbook of Computer Science and Engineering},
  chapter = {139},
  publisher = {CRC Press},
  year = {1996},
  editor = {Allen B. Tucker},
  plclub = {Yes},
  bcp = {Yes},
  full = {http://www.cis.upenn.edu/~bcpierce/papers/crchandbook.ps},
  keys = {pict}
}
@article{CompagnoniPierce93,
  author = {Adriana B. Compagnoni and Benjamin C. Pierce},
  title = {Intersection Types and Multiple Inheritance},
  pages = {469--501},
  journal = {Mathematical Structures in Computer Science},
  month = oct,
  year = 1996,
  volume = 6,
  number = 5,
  source = {http://theory.lcs.mit.edu/~dmjones/hbp/mscs/mscs.bib},
  note = {Preliminary version available as University of Edinburgh
                  technical report ECS-LFCS-93-275 and Catholic University
                  Nijmegen computer science technical report 93-18, Aug.
                  1993, under the title ``Multiple Inheritance via
                  Intersection Types''},
  plclub = {Yes},
  bcp = {Yes}
}
@inproceedings{KobayashiPierceTurner:LinearPi,
  author = {Naoki Kobayashi and Benjamin C. Pierce and David N.
                  Turner},
  title = {Linearity and the Pi-Calculus},
  year = {1996},
  booktitle = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
                     {L}anguages ({POPL}), St.~Petersburg Beach, Florida},
  note = {Full version in \bgroup\em ACM Transactions on Programming Languages and Systems\egroup, 21(5), pp. 914--947, September 1999},
  plclub = {Yes},
  bcp = {Yes}
}
@article{CompagnoniPierce93:old,
  author = {Adriana B. Compagnoni and Benjamin C. Pierce},
  title = {Multiple Inheritance via Intersection Types},
  journal = {Mathematical Structures in Computer Science},
  year = 1996,
  note = {To appear. Preliminary version available as University of
                  Edinburgh technical report ECS-LFCS-93-275 and Catholic
                  University Nijmegen computer science technical report
                  93-18, Aug. 1993},
  plclub = {Yes},
  bcp = {Yes}
}
@article{OnBinaryMethods,
  author = {Kim B. Bruce and Luca Cardelli and Giuseppe Castagna and
                  {the Hopkins Objects Group (Jonathan Eifrig, Scott Smith,
                  Valery Trifonov)} and Gary T. Leavens and Benjamin Pierce},
  title = {On Binary Methods},
  journal = {Theory and Practice of Object Systems},
  volume = 1,
  number = 3,
  pages = {221--242},
  year = 1996,
  checked = {No},
  plclub = {Yes},
  bcp = {Yes},
  keys = {oop},
  ps = {http://www.cis.upenn.edu/~bcpierce/papers/binary.ps}
}
@misc{Pierce:FMOODSTalk,
  author = {Benjamin C. Pierce},
  title = {Processes, Types, and Observations},
  note = {Invited lecture at {\em Formal Methods on Open,
                  Object-Based Distributed Systems (FMOODS)}, Paris},
  year = 1996,
  month = mar,
  plclub = {Yes},
  bcp = {Yes}
}
@unpublished{Pierce96a,
  author = {Benjamin C. Pierce},
  title = {Types},
  note = {Lecture notes for an undergraduate course at Cambridge
                  University},
  month = feb,
  year = 1996,
  plclub = {Yes},
  bcp = {Yes}
}
@inproceedings{PierceSangiorgi96,
  author = {Benjamin Pierce and Davide Sangiorgi},
  title = {Behavioral Equivalence in the Polymorphic Pi-Calculus},
  year = 1997,
  booktitle = {Principles of Programming Languages (POPL)},
  note = {Full version in {\em Journal of the Association for
                  Computing Machinery (JACM)}, 47(3), May 2000},
  pages = {531--584},
  full = {http://www.cis.upenn.edu/~bcpierce/papers/polybisim.ps},
  plclub = {Yes},
  bcp = {Yes},
  keys = {pict}
}
@techreport{Pierce:BQB,
  author = {Benjamin C. Pierce},
  title = {Bounded Quantification with Bottom},
  year = {1997},
  institution = {Computer Science Department, Indiana University},
  series = {CSCI},
  number = {492},
  plclub = {Yes},
  bcp = {Yes},
  keys = {subtyping},
  tr = {http://www.cis.upenn.edu/~bcpierce/papers/bqb.ps}
}
@inproceedings{BruceCardelliPierce96:TACS,
  author = {Kim B. Bruce and Luca Cardelli and Benjamin C. Pierce},
  title = {Comparing Object Encodings},
  booktitle = {International Symposium on Theoretical Aspects of Computer Software (TACS)},
  year = 1997,
  month = sep,
  note = {An earlier version was presented as an invited lecture at
                  the Third International Workshop on Foundations of Object
                  Oriented Languages (FOOL 3), July 1996; full version in \bgroup\em Information and Computation\egroup, 155(1--2):108-133, 1999},
  plclub = {Yes},
  bcp = {Yes}
}
@article{PierceSteffen95:old,
  author = {Benjamin Pierce and Martin Steffen},
  title = {Higher-Order Subtyping},
  year = 1997,
  journal = {Theoretical Computer Science},
  volume = 176,
  number = {1--2},
  pages = {235--282},
  note = {Summary in IFIP Working Conference on Programming
                  Concepts, Methods and Calculi (PROCOMET), June 1994; also
                  University of Edinburgh technical report ECS-LFCS-94-280
                  and {Universit\"at Erlangen-N\"urnberg Interner Bericht
                  IMMD7-01/94}, January 1994.},
  plclub = {Yes},
  bcp = {Yes}
}
@article{Pierce92b,
  author = {Benjamin C. Pierce},
  title = {Intersection Types and Bounded Polymorphism},
  pages = {129--193},
  journal = {Mathematical Structures in Computer Science},
  month = apr,
  year = 1997,
  volume = 7,
  number = 2,
  source = {http://theory.lcs.mit.edu/~dmjones/hbp/mscs/mscs.bib},
  note = {Summary in {\em Typed Lambda
                  Calculi and Applications}, March 1993, pp. 346--360},
  ascii = {Benjamin C. Pierce, "Intersection Types and Bounded
                  Polymorphism." Conference on Typed Lambda Calculi and
                  Applications, March, 1993},
  plclub = {Yes},
  bcp = {Yes}
}
@misc{Pierce:LFPTW,
  author = {Benjamin C. Pierce},
  title = {Languages for Programming the Web},
  month = dec,
  year = {1997},
  note = {Course materials for a graduate seminar on the theory and
                  practice of mobile agent programming. Available through
                  {\tt http://www.cis.upenn.edu/$sim$bcpierce/courses/629}.},
  plclub = {Yes},
  bcp = {Yes}
}
@techreport{PierceTurner:LTI-FSUB,
  author = {Benjamin C. Pierce and David N. Turner},
  title = {Local Type Argument Synthesis with Bounded Quantification},
  year = {1997},
  institution = {Computer Science Department, Indiana University},
  month = jan,
  series = {CSCI},
  number = {495},
  plclub = {Yes},
  bcp = {Yes},
  tr = {http://www.cis.upenn.edu/~bcpierce/papers/lti-fsub.ps},
  keys = {inference}
}
@techreport{PierceTurner:LTI-TR,
  author = {Benjamin C. Pierce and David N. Turner},
  title = {Local Type Inference},
  year = {1997},
  institution = {Computer Science Department, Indiana University},
  series = {CSCI},
  number = {493},
  plclub = {Yes},
  bcp = {Yes}
}
@unpublished{PierceTurner:PictDefn,
  author = {Benjamin C. Pierce and David N. Turner},
  title = {Pict Language Definition},
  year = {1997},
  note = {Available electronically},
  plclub = {Yes},
  bcp = {Yes}
}
@unpublished{PierceTurner:PictLib,
  author = {Benjamin C. Pierce and David N. Turner},
  title = {Pict Libraries Manual},
  year = {1997},
  note = {Available electronically},
  plclub = {Yes},
  bcp = {Yes}
}
@misc{PierceTurner:PictCompiler,
  author = {Benjamin C. Pierce and David N. Turner},
  title = {Pict: A Programming Language Based on the Pi-Calculus},
  year = {1997},
  note = {\URL{http://www.cis.upenn.edu/~bcpierce/papers/pict}},
  plclub = {Yes},
  bcp = {Yes}
}
@misc{PictDistribution,
  author = {Benjamin C. Pierce and David N. Turner},
  title = {The {Pict} Programming Language},
  year = {2001},
  homepage = {http://www.cis.upenn.edu/~bcpierce/papers/pict/Html/Pict.html},
  plclub = {Yes},
  bcp = {Yes},
  keys = {pict},
  note = {This directory contains various papers, including a tutorial and user's manual, as well as complete compiler sources and installation instructions. (Be sure not to miss the artwork department!)}
}
@unpublished{Pierce94b,
  author = {Benjamin C. Pierce},
  title = {Programming in the Pi-Calculus: {A} Tutorial Introduction
                  to {P}ict},
  year = {1997},
  note = {Available electronically},
  plclub = {Yes},
  bcp = {Yes}
}
@article{Pierce98:ACReview,
  author = {Benjamin C. Pierce},
  title = {Review of {A Theory of Objects}, by {A}badi and
                  {C}ardelli},
  year = {1997},
  volume = 40,
  number = 5,
  pages = {297--298},
  journal = {The Computer Journal},
  source = {Tom Melham},
  plclub = {Yes},
  bcp = {Yes},
  keys = {oop},
  ps = {http://www.cis.upenn.edu/~bcpierce/papers/ac-review.ps}
}
@article{GhelliPierce95-OLD,
  author = {Giorgio Ghelli and Benjamin Pierce},
  title = {Bounded Existentials and Minimal Typing},
  year = {1998},
  volume = 193,
  pages = {75--96},
  journal = {Theoretical Computer Science},
  plclub = {Yes},
  bcp = {Yes},
  note = {Circulated in manuscript form in 1992}
}
@misc{GhelliPierce95,
  author = {Giorgio Ghelli and Benjamin Pierce},
  title = {Bounded Existentials and Minimal Typing},
  year = {1992},
  note = {Circulated in manuscript form. Full version in
                  {\em Theoretical Computer Science}, 193(1--2):75--96, February 1998.},
  plclub = {Yes},
  bcp = {Yes},
  keys = {subtyping},
  ps = {http://www.cis.upenn.edu/~bcpierce/papers/exists.ps}
}
@techreport{BalasubramaniamPierce98-TR,
  author = {S. Balasubramaniam and Benjamin C. Pierce},
  title = {File Synchronization},
  institution = {Computer Science Department, Indiana University},
  series = {CSCI},
  number = {507},
  month = apr,
  year = 1998,
  plclub = {Yes},
  bcp = {Yes}
}
@inproceedings{PierceTurner:LTI,
  author = {Benjamin C. Pierce and David N. Turner},
  title = {Local Type Inference},
  year = 1998,
  booktitle = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
                     {L}anguages ({POPL}), San Diego, California},
  note = {Full version in \bgroup\em ACM Transactions on Programming
                  Languages and Systems (TOPLAS)\egroup, 22(1), January 2000,
                  pp.~1--44},
  plclub = {Yes},
  bcp = {Yes},
  keys = {inference},
  tr = {http://www.cis.upenn.edu/~bcpierce/papers/lti.pdf},
  conf = {http://www.cis.upenn.edu/~bcpierce/papers/lti-popl.pdf},
  full = {http://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf}
}
@inproceedings{HofmannPierce:TD,
  author = {Martin Hofmann and Benjamin C. Pierce},
  title = {Type Destructors},
  booktitle = {Informal proceedings of the Fourth International Workshop
                  on Foundations of Object-Oriented Languages (FOOL)},
  editor = {Didier R\'e{}my},
  month = jan,
  year = {1998},
  note = {Full version in {\em Information and Computation}, 172(1)29--62 (2002)},
  plclub = {Yes},
  bcp = {Yes},
  keys = {oop},
  conf = {http://www.cis.upenn.edu/~bcpierce/papers/td.ps}
}
@misc{Pierce:CONCUR-tutorial,
  author = {Benjamin C. Pierce},
  title = {Type Systems for Concurrent Calculi},
  month = sep,
  year = {1998},
  note = {Invited tutorial at {\em CONCUR}, Nice, France},
  plclub = {Yes},
  bcp = {Yes}
}
@incollection{BunemanPierce99,
  author = {Peter Buneman and Benjamin Pierce},
  booktitle = {Internet Programming Languages},
  title = {Union Types for Semistructured Data},
  year = {1998},
  month = sep,
  publisher = {Springer-Verlag},
  note = {Proceedings of the International Database Programming
                  Languages Workshop. LNCS 1686},
  plclub = {Yes},
  bcp = {Yes},
  keys = {xduce},
  conf = {http://www.cis.upenn.edu/~bcpierce/papers/utssd.ps}
}
@inproceedings{BalasubramaniamPierce98,
  author = {S. Balasubramaniam and Benjamin C. Pierce},
  title = {What is a file synchronizer?},
  booktitle = {Fourth Annual ACM/IEEE International Conference on Mobile
                  Computing and Networking (MobiCom '98)},
  month = oct,
  year = 1998,
  note = {Full version available as Indiana University CSCI
                  technical report \#507, April 1998},
  conf = {http://www.cis.upenn.edu/~bcpierce/papers/snc-mobicom.ps},
  tr = {http://www.cis.upenn.edu/~bcpierce/papers/snc.ps},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/snc-slides.ps},
  keys = {unison},
  plclub = {Yes},
  bcp = {Yes}
}
@misc{Pierce:GlobalComputingFoolTalk,
  author = {Benjamin C. Pierce},
  title = {Global Computing: Some Questions for {FOOLs}},
  slides = {gc-fool-slides.ps},
  plclub = {Yes},
  bcp = {Yes},
  keys = {concurrencysurveys},
  note = {Invited talk at FOOL workshop},
  year = 2001
}
@misc{Pierce:TypeSystemsForConcurrencyTalk,
  author = {Benjamin C. Pierce},
  title = {Type Systems for Concurrent Calculi},
  slides = {concur98.ps},
  plclub = {Yes},
  bcp = {Yes},
  keys = {concurrencysurveys},
  note = {Invited tutorial at CONCUR},
  year = 1998
}
@misc{Pierce:FileSyncTheoryAndPracticeSlides,
  author = {Benjamin C. Pierce},
  title = {File Synchronization: Theory and Practice},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/new-snc-slides.ps},
  plclub = {Yes},
  bcp = {Yes},
  keys = {unison},
  year = 2001
}
@misc{Pierce:UnisonAFileSync-Slides,
  author = {Benjamin C. Pierce},
  title = {Unison: A file synchronizer and its specification},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/snc-tacs-2001Oct.ps},
  note = {Invited talk at {\em Theoretical Aspects of Computer Software}
                  (TACS), Sendai, Japan},
  plclub = {Yes},
  bcp = {Yes},
  keys = {unison},
  year = 2001
}
@misc{Pierce:snc,
  author = {Benjamin C. Pierce and Sundar Balasubramaniam, Trevor Jim
                  and Insup Lee and Insik Shin},
  title = {{\sc Snc}: a file synchronizer},
  year = {1998},
  note = {(Superseded by {\sc Unison}.)},
  plclub = {Yes},
  bcp = {Yes}
}
@inproceedings{IgarashiPierceWadler99,
  author = {Atsushi Igarashi and Benjamin Pierce and Philip Wadler},
  title = {Featherweight {J}ava: {A} Minimal Core Calculus for {J}ava
                  and {GJ}},
  month = oct,
  booktitle = {{ACM} {SIGPLAN} {C}onference on {O}bject {O}riented {P}rogramming:
                    {S}ystems, {L}anguages, and {A}pplications ({OOPSLA})},
  year = {1999},
  note = {Full version in ACM Transactions on Programming
                  Languages and Systems (TOPLAS), 23(3), May 2001},
  plclub = {Yes},
  bcp = {Yes},
  keys = {oop},
  conf = {http://www.cis.upenn.edu/~bcpierce/papers/fj-oopsla.ps},
  full = {http://www.cis.upenn.edu/~bcpierce/papers/fj-toplas.pdf}
}
@inproceedings{IgarashiPierce99,
  author = {Atsushi Igarashi and Benjamin C. Pierce},
  title = {Foundations for Virtual Types},
  month = jun,
  year = 1999,
  booktitle = {European Conference on Object-Oriented Programming (ECOOP), Lisbon, Portugal},
  note = {Also in informal proceedings of the
                  {\em Workshop on Foundations of Object-Oriented Languages
                  (FOOL)}, January 1999. Full version in {\em Information and
                  Computation}, 175(1): 34--49, May 2002},
  plclub = {Yes},
  bcp = {Yes},
  keys = {oop},
  ps = {http://www.cis.upenn.edu/~bcpierce/papers/vt.ps}
}
@techreport{HosoyaPierce99,
  author = {Haruo Hosoya and Benjamin C. Pierce},
  title = {How Good is Local Type Inference?},
  institution = {University of Pennsylvania},
  number = {MS-CIS-99-17},
  month = jun,
  year = 1999,
  plclub = {Yes},
  bcp = {Yes},
  keys = {inference},
  tr = {http://www.cis.upenn.edu/~bcpierce/papers/hgilti.ps}
}
@article{KobayashiPierceTurner:LinearPi:TOPLAS,
  author = {Naoki Kobayashi and Benjamin C. Pierce and David N.
                  Turner},
  title = {Linearity and the {Pi-Calculus}},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {21},
  number = {5},
  pages = {914--947},
  month = sep,
  year = {1999},
  coden = {ATPSDT},
  fullissn = {0164-0925},
  bibdate = {Tue Sep 26 10:12:58 MDT 2000},
  source = {TOPLAS db},
  note = {Summary in POPL 1996.},
  keys = {pict},
  full = {http://www.acm.org/pubs/articles/journals/toplas/1999-21-5/p914-kobayashi/p914-kobayashi.pdf;
                  http://www.acm.org/pubs/citations/journals/toplas/1999-21-5/p914-kobayashi/},
  abstract = {The economy and flexibility of the pi-calculus make it an
                  attractive object of theoretical study and a clean basis
                  for concurrent language design and implementation. However,
                  such generality has a cost: encoding higher-level features
                  like functional computation in pi-calculus throws away
                  potentially useful information. We show how a linear type
                  system can be used to recover important static information
                  about a process's behavior. In particular, we can guarantee
                  that two processes communicating over a linear channel
                  cannot interfere with other communicating processes. After
                  developing standard results such as soundness of typing, we
                  focus on equivalences, adapting the standard notion of
                  barbed bisimulation to the linear setting and showing how
                  reductions on linear channels induce a useful ``partial
                  confluence'' of process behaviors. For an extended example
                  of the theory, we prove the validity of a tail-call
                  optimization for higher-order functions represented as
                  processes.},
  plclub = {Yes},
  bcp = {Yes}
}
@inproceedings{SewellWojciechowskiPierce98,
  author = {Peter Sewell and Pawel Wojciechowski and Benjamin Pierce},
  title = {Location Independence for Mobile Agents},
  booktitle = {Proceedings of {ICCL} '98},
  editor = {H. E. Bal and B. Belkhouche and L. Cardelli},
  volume = {1686},
  series = {lncs},
  publisher = {Springer-Verlag},
  month = sep,
  year = {1999},
  note = {An earlier version with title {\em Location-Independent
                  Communication for Mobile Agents: a Two-Level
                  Architecture\/} appeared as Technical Report 462, Computer
                  Laboratory, University of Cambridge, April 1999},
  plclub = {Yes},
  bcp = {Yes},
  tr = {http://www.cis.upenn.edu/~bcpierce/papers/wipl.ps},
  official = {http://link.springer.de/link/service/series/0558/bibs/1686/16860001.htm},
  keys = {mobileagents}
}
@techreport{SewellWojciechowskiPierce98:TR,
  author = {Peter Sewell and Pawe{\l} T. Wojciechowski and Benjamin C.
                  Pierce},
  title = {Location-Independent Communication for Mobile Agents: a
                  Two-Level Architecture},
  institution = {Computer Laboratory, University of Cambridge},
  year = {1999},
  number = {462},
  plclub = {Yes},
  bcp = {Yes}
}
@misc{HarmonyRelationsPoster,
  author = {Aaron Bohannon and Jeffrey A. Vaughan and
                  Benjamin C. Pierce},
  title = {Relational Lenses: {A} language for defining
                  updateable views},
  year = {2005},
  month = oct,
  note = {Poster presented at Greater Philadelphia DB/IR Day},
  bcp = {Yes},
  keys = {harmony},
  pdf = {http://www.cis.upenn.edu/~bcpierce/papers/harmony-relations-dbir-poster.pdf}
}
@inproceedings{BohannonPierceVaughan,
  author = {Aaron Bohannon and Jeffrey A. Vaughan and
                  Benjamin C. Pierce},
  title = {Relational Lenses: {A} Language for Updateable Views},
  year = {2006},
  booktitle = {Principles of Database Systems (PODS)},
  note = {Extended version available as University of Pennsylvania
                  technical report MS-CIS-05-27},
  bcp = {Yes},
  plclub = {Yes},
  keys = {harmony},
  pdf = {http://www.cis.upenn.edu/~bcpierce/papers/dblenses-pods.pdf},
  tr = {http://www.cis.upenn.edu/~bcpierce/papers/dblenses-tr.pdf}
}
@misc{SahuguetPierceTannen2000,
  author = {Arnaud Sahuguet and Benjamin Pierce and Val Tannen},
  title = {Chaining, Referral, Subscription, Leasing: New Mechanisms
                  in Distributed Query Optimization},
  month = feb,
  year = {2000},
  plclub = {Yes},
  bcp = {Yes}
}
@misc{SahuguetPierceTannen2000a,
  author = {Arnaud Sahuguet and Benjamin Pierce and Val Tannen},
  title = {Distributed Query Optimization: Can Mobile Agents Help?},
  month = feb,
  year = {2000},
  plclub = {Yes},
  bcp = {Yes}
}
@inproceedings{SewellWojciechowskiPierce98:old,
  author = {Peter Sewell and Pawel T. Wojciechowski and Benjamin C.
                  Pierce},
  title = {Location Independence for Mobile Agents},
  year = 2000,
  note = {To appear in an edited collection of papers (in Springer
                  LNCS) from the {\em Workshop on Internet Programming
                  Languages}, June 1998, Loyola University},
  plclub = {Yes},
  bcp = {Yes}
}
@misc{Pierce:ICFP-invited,
  author = {Benjamin C. Pierce},
  title = {Module Systems: A Guide for the Perplexed},
  month = sep,
  year = {2000},
  note = {Invited talk at {\em ICFP}, Montreal},
  plclub = {Yes},
  bcp = {Yes}
}
@article{IgarashiPierce99:FJI,
  author = {Atsushi Igarashi and Benjamin C. Pierce},
  title = {On Inner Classes},
  journal = {Information and Computation},
  year = 2002,
  volume = 177,
  number = 1,
  pages = {56--89},
  month = aug,
  note = {A special issue with papers from the 7th International Workshop on Foundations of Object-Oriented Languages (FOOL){\rm, informal proceedings}.  An earlier
                  version appeared in \emph \bgroup Proceedings of the 14th European Conference on Object-Oriented Programming (ECOOP)\egroup, Springer LNCS 1850, pages
                  129--153},
  plclub = {Yes},
  bcp = {Yes},
  keys = {oop},
  conf = {http://www.cis.upenn.edu/~bcpierce/fji.ps},
  tr = {http://www.cis.upenn.edu/~bcpierce/fji-tr.ps}
}
@incollection{PierceTurner:PictDesign,
  author = {Benjamin C. Pierce and David N. Turner},
  title = {Pict: A Programming Language Based on the Pi-Calculus},
  year = {2000},
  booktitle = {Proof, Language and Interaction: Essays in Honour of Robin
                  Milner},
  editor = {Gordon Plotkin and Colin Stirling and Mads Tofte},
  publisher = {MIT Press},
  pages = {455--494},
  checked = {Yes},
  plclub = {Yes},
  bcp = {Yes},
  full = {http://www.cis.upenn.edu/~bcpierce/papers/pict-design.ps},
  keys = {pict}
}
@article{GapeyevLevinPierce2000,
  author = {Vladimir Gapeyev and Michael Levin and Benjamin Pierce},
  title = {Recursive Subtyping Revealed},
  journal = {Journal of Functional Programming},
  volume = 12,
  number = 6,
  pages = {511--548},
  checked = {Yes},
  year = {2003},
  plclub = {Yes},
  bcp = {Yes},
  keys = {subtyping},
  conf = {http://www.cis.upenn.edu/~bcpierce/papers/rsr.ps},
  note = {Preliminary version in {\em International Conference on
                  Functional Programming (ICFP)}, 2000.  Also appears as
                  Chapter 21 of {\em Types and Programming Languages}
                  by Benjamin C. Pierce (MIT Press, 2002).}
}
@inproceedings{GapeyevLevinPierce2000:ICFP,
  author = {Vladimir Gapeyev and Michael Levin and Benjamin Pierce},
  title = {Recursive Subtyping Revealed},
  booktitle = {{ACM} {SIGPLAN} {I}nternational {C}onference on {F}unctional {P}rogramming
                    ({ICFP}), Montreal, Canada},
  year = {2000},
  plclub = {Yes},
  bcp = {Yes},
  note = {To appear in {\em Journal of Functional Programming}}
}
@misc{PierceSumii00,
  author = {Benjamin Pierce and Eijiro Sumii},
  title = {Relating Cryptography and Polymorphism},
  month = jul,
  year = {2000},
  plclub = {Yes},
  bcp = {Yes},
  note = {Some parts superseded by \cite{SumiiPierce01} (Sumii and Pierce, 2001)},
  keys = {security},
  manuscript = {http://www.cis.upenn.edu/~bcpierce/papers/infohide.ps}
}
@techreport{LevinPierce99:OLD1,
  author = {Michael Y. Levin and Benjamin C. Pierce},
  title = {TinkerType: {A} Language for Playing with Formal Systems},
  month = jun,
  year = {2000},
  booktitle = {Logical Frameworks and Metalanguages},
  note = {Invited talk (submitted for journal publication)},
  plclub = {Yes},
  bcp = {Yes}
}
@inproceedings{HosoyaPierce2000,
  author = {Haruo Hosoya and Benjamin C. Pierce},
  title = {{XDuce}: A Typed {XML} Processing Language (Preliminary
                  Report)},
  booktitle = {International Workshop on the Web and Databases (WebDB)},
  editor = {Dan Suciu and Gottfried Vossen},
  month = may,
  year = {2000},
  note = {Reprinted in {\em The Web and Databases, Selected Papers},
                  Springer LNCS volume 1997, 2001},
  keys = {xduce},
  conf = {http://www.cis.upenn.edu/~bcpierce/papers/xduce-prelim.ps},
  plclub = {Yes},
  bcp = {Yes}
}
@inproceedings{IgarashiPierceWadler01,
  author = {Atsushi Igarashi and Benjamin C. Pierce and Philip Wadler},
  title = {A Recipe for Raw Types},
  year = 2001,
  booktitle = {Workshop on Foundations of Object-Oriented Languages
                  (FOOL)},
  plclub = {Yes},
  bcp = {Yes},
  keys = {oop},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/rfgj.ps}
}
@article{BruceCardelliPierce96,
  author = {Kim B. Bruce and Luca Cardelli and Benjamin C. Pierce},
  title = {Comparing Object Encodings},
  journal = {Information and Computation},
  year = 1999,
  month = nov,
  volume = 155,
  number = {1/2},
  pages = {108--133},
  note = {Special issue of papers from {\em
                  Theoretical Aspects of Computer Software (TACS 1997)}.
                  An earlier version appeared as an invited
                  lecture in the Third International Workshop on Foundations
                  of Object Oriented Languages (FOOL 3), July 1996},
  plclub = {Yes},
  bcp = {Yes},
  keys = {oop},
  ps = {http://www.cis.upenn.edu/~bcpierce/papers/compobj.ps}
}
@unpublished{JimPierceVouillon:UnisonSys,
  author = {Trevor Jim and Benjamin C. Pierce and J\'er\^ome Vouillon},
  title = {How to Build a File Synchronizer},
  year = {2003},
  note = {Manuscript},
  plclub = {Yes},
  bcp = {Yes}
}
@article{SumiiPierce01,
  author = {Eijiro Sumii and Benjamin C. Pierce},
  title = {Logical Relations for Encryption},
  journal = {Journal of Computer Security},
  year = {2003},
  volume = {11},
  number = {4},
  pages = {521--554},
  plclub = {Yes},
  bcp = {Yes},
  conf = {http://www.cis.upenn.edu/~bcpierce/papers/infohide2.ps},
  keys = {security},
  note = {Extended abstract appeared in {\emph{14th IEEE Computer Security Foundations Workshop}}, pp.~256--269, 2001.}
}
@inproceedings{HosoyaPierce2001,
  author = {Haruo Hosoya and Benjamin C. Pierce},
  title = {Regular Expression Pattern Matching},
  booktitle = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
                     {L}anguages ({POPL}), London, England},
  year = {2001},
  plclub = {Yes},
  bcp = {Yes},
  checked = {Yes},
  note = {Full version in {\em Journal of
                  Functional Programming}, 13(6), Nov. 2003, pp. 961--1004},
  full = {http://www.cis.upenn.edu/~bcpierce/papers/tapat.ps},
  keys = {xduce}
}
@article{HosoyaVouillonPierce2000,
  author = {Haruo Hosoya and J\'er\^ome Vouillon and Benjamin C.
                  Pierce},
  title = {Regular Expression Types for {XML}},
  journal = {ACM Transactions on Programming Languages and Systems
                  (TOPLAS)},
  year = {2005},
  month = jan,
  volume = 27,
  number = 1,
  pages = {46--90},
  note = {Preliminary version in ICFP 2000},
  plclub = {Yes},
  bcp = {Yes},
  checked = {Yes},
  keys = {xduce},
  conf = {http://www.cis.upenn.edu/~bcpierce/papers/regsub.ps},
  full = {http://www.cis.upenn.edu/~bcpierce/papers/regsub-toplas.pdf}
}
@article{HosoyaPierce2002,
  author = {Haruo Hosoya and Benjamin C. Pierce},
  title = {{XDuce}: A Statically Typed {XML} Processing Language},
  journal = {ACM Transactions on Internet Technology},
  year = {2003},
  volume = 3,
  number = 2,
  month = may,
  pages = {117--148},
  checked = {Yes},
  official = {http://doi.acm.org/10.1145/767193.767195},
  plclub = {Yes},
  bcp = {Yes},
  keys = {xduce}
}
@inproceedings{Pierce-Sumii-01,
  author = {Eijiro Sumii and Benjamin Pierce},
  title = {The Cryptographic {$\lambda$}-Calculus: Syntax, Semantics,
                  Type System and Logical Relation (in Japanese)},
  booktitle = {Informal Proceedings of JSSST Workshop on Programming and
                  Programming Languages (PPL2001)},
  year = {2001},
  note = {Best paper prize},
  plclub = {Yes},
  bcp = {Yes}
}
@misc{XtaticCompiler,
  author = {Vladimir Gapeyev and Michael Y. Levin and Benjamin C. Pierce and Alan Schmitt},
  title = {The {X}tatic Compiler and Runtime System},
  year = {2005},
  plclub = {Yes},
  bcp = {Yes},
  keys = {xtatic},
  sources = {http://www.cis.upenn.edu/~bcpierce/papers/xtatic.tgz}
}
@phdthesis{LevinThesis,
  author = {Michael Y. Levin},
  title = {Run, Xtatic, Run: Efficient Implementation of an Object-Oriented
                  Language with Regular Pattern Matching},
  school = {University of Pennsylvania},
  year = {2005},
  bcp = {Yes},
  keys = {xtatic},
  plclub = {Yes},
  pdf = {http://www.cis.upenn.edu/~bcpierce/papers/levin-thesis.pdf}
}
@inproceedings{GapeyevPierce03,
  author = {Vladimir Gapeyev and Benjamin C. Pierce},
  title = {Regular Object Types},
  booktitle = {European Conference on Object-Oriented Programming (ECOOP), Darmstadt, Germany},
  year = {2003},
  note = {A preliminary version was presented at FOOL '03},
  plclub = {Yes},
  bcp = {Yes},
  keys = {xtatic},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/regobj.pdf},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/regobj-ecoop-slides.ps}
}
@article{LevinPierce99,
  author = {Michael Y. Levin and Benjamin C. Pierce},
  title = {TinkerType: {A} Language for Playing with Formal Systems},
  journal = {Journal of Functional Programming},
  volume = 13,
  number = 2,
  month = mar,
  year = {2003},
  note = {A preliminary version appeared as an invited
                  paper at the {\em Logical Frameworks and Metalanguages
                  Workshop (LFM)}, June 2000},
  plclub = {Yes},
  bcp = {Yes},
  full = {http://www.cis.upenn.edu/~bcpierce/papers/tt-jfp.pdf},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/tt-slides.ps},
  sources = {http://www.cis.upenn.edu/~bcpierce/papers/tt.tar.gz},
  keys = {modular}
}
@unpublished{PierceVouillon:UnisonSpec,
  author = {Benjamin C. Pierce and J\'er\^ome Vouillon},
  title = {Unison: A File Synchronizer and its Specification},
  year = {2001},
  note = {Manuscript},
  plclub = {Yes},
  bcp = {Yes}
}
@techreport{PierceVouillon:UnisonSpecTR,
  author = {Benjamin C. Pierce and J\'er\^ome Vouillon},
  title = {What's in {U}nison? {A} Formal
                  Specification and Reference Implementation
                  of a File Synchronizer},
  year = {2004},
  institution = {Dept. of Computer and Information Science, University of Pennsylvania},
  number = {MS-CIS-03-36},
  plclub = {Yes},
  bcp = {Yes},
  tr = {http://www.cis.upenn.edu/~bcpierce/papers/unisonspec.pdf},
  keys = {unison}
}
@book{Pierce:TypeSystems,
  author = {Benjamin C. Pierce},
  title = {Types and Programming Languages},
  publisher = {MIT Press},
  year = 2002,
  plclub = {Yes},
  bcp = {Yes},
  keys = {books},
  homepage = {http://www.cis.upenn.edu/~bcpierce/tapl},
  errata = {http://www.cis.upenn.edu/~bcpierce/tapl/errata.txt}
}
@book{ATTAPL,
  editor = {Benjamin C. Pierce},
  title = {Advanced Topics in Types and Programming Languages},
  publisher = {MIT Press},
  year = 2005,
  plclub = {Yes},
  bcp = {Yes},
  keys = {books},
  homepage = {http://www.cis.upenn.edu/~bcpierce/attapl}
}
@proceedings{ISSS2002,
  title = {Software Security -- Theories and Systems},
  editor = {M. Okada and B. Pierce and A. Scedrov and H. Tokuda
                  and A. Yonezawa},
  series = {Lecture Notes in Computer Science},
  number = {2609},
  publisher = {Springer-Verlag},
  optaddress = {Berlin},
  year = {2003},
  note = {Revised papers from the Mext-NSF-JSPS {\em International
                  Symposium on Software Security}, Tokyo, Japan,
                  November 8-10, 2002},
  isbn = {3-540-00708-3},
  plclub = {Yes},
  bcp = {Yes}
}
@proceedings{TACS2001,
  title = {Theoretical Aspects of
                  Computer Software (TACS), 4th International Symposium},
  editor = {Naoki Kobayashi and Benjamin C. Pierce},
  series = {Lecture Notes in Computer Science},
  number = {2215},
  publisher = {Springer-Verlag},
  optaddress = {Berlin},
  year = {2001},
  location = {Sendai, Japan, October 29-31, 2001},
  isbn = {3-540-42736-8},
  plclub = {Yes},
  bcp = {Yes}
}
@inproceedings{nwaysync,
  booktitle = {International Symposium on Distributed Computing (DISC)},
  editor = {Shlomi Dolev},
  author = {Michael B. Greenwald and Sanjeev Khanna and
                  Keshav Kunal and Benjamin C. Pierce and Alan Schmitt},
  title = {Agreeing to Agree: {C}onflict Resolution for
                  Optimistically Replicated Data},
  keys = {unison},
  plclub = {Yes},
  bcp = {Yes},
  year = 2006,
  short = {http://www.cis.upenn.edu/~bcpierce/papers/nway-disc.pdf},
  tr = {http://www.cis.upenn.edu/~bcpierce/papers/nway-tr.pdf},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/nway-disc-slides.pdf}
}
@inproceedings{diff3,
  author = {Sanjeev Khanna and Keshav Kunal and Benjamin C. Pierce},
  title = {A Formal Investigation of Diff3},
  year = 2007,
  month = dec,
  short = {http://www.cis.upenn.edu/~bcpierce/papers/diff3-short.pdf},
  plclub = {Yes},
  bcp = {Yes},
  keys = {unison},
  booktitle = {Foundations of Software Technology and Theoretical Computer Science (FSTTCS)},
  editor = {Arvind and Prasad}
}
@article{Focal2005-long,
  author = {J. Nathan Foster and Michael B. Greenwald and Jonathan T. Moore
                  and Benjamin C. Pierce and Alan Schmitt},
  title = {Combinators for bidirectional tree transformations:
                  {A} linguistic approach to the view-update problem},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {29},
  number = {3},
  pages = {17},
  month = may,
  year = {2007},
  publisher = {ACM Press},
  address = {New York, NY, USA},
  conf = {http://www.cis.upenn.edu/~bcpierce/papers/newlenses-popl.pdf},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/newlenses-popl-slides.pdf},
  full = {http://www.cis.upenn.edu/~bcpierce/papers/lenses-toplas-final.pdf},
  fullappendix = {http://www.cis.upenn.edu/~bcpierce/papers/lenses-toplas-electronic-appendix.pdf},
  doi = {http://portal.acm.org/citation.cfm?doid=1232420.1232424},
  note = {Preliminary version presented at
                  the {\em Workshop on Programming Language Technologies for
                  XML (PLAN-X)}, 2004; extended abstract presented at
                  {\em Principles of Programming Languages (POPL)}, 2005},
  bcp = {Yes},
  plclub = {Yes},
  keys = {harmony}
}
@misc{Pierce:NEPLS2004,
  author = {Benjamin C. Pierce},
  title = {Combinators for Bi-Directional Tree Transformations:
                  {A} Linguistic Approach to the View Update Problem},
  month = oct,
  year = 2004,
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/newlenses-slides.pdf},
  note = {Invited talk at {\em New England Programming Languages Symposium}},
  plclub = {Yes},
  bcp = {Yes},
  keys = {harmony}
}
@misc{Pierce:LinksTalk2005,
  author = {Benjamin C. Pierce},
  title = {Fancy Types for XML: Friend or Foe?},
  month = apr,
  year = 2005,
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/linkstalk-200504.pdf},
  note = {Talk at {\em LINKS} workshop, April 2005},
  plclub = {Yes},
  bcp = {Yes},
  keys = {xtatic}
}
@misc{Pierce:HarmonyTalkTGC,
  author = {Benjamin C. Pierce},
  title = {Harmony: {T}he Art of Reconciliation},
  month = apr,
  year = 2005,
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/harmony-tgc-talk-2005.pdf},
  note = {Invited talk at {\em Trusted Global Computing} conference,
                  April 2005},
  plclub = {Yes},
  bcp = {Yes},
  keys = {unison}
}
@misc{Pierce:HarmonyTalk2003,
  author = {Benjamin C. Pierce},
  title = {Harmony: A Synchronization Framework for Tree-Structured Data},
  month = sep,
  year = 2003,
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/harmonyslides-2003aug.pdf},
  note = {Slides from a talk presented in several places
                  (Cambridge, Edinburgh,
                  Philadelphia, Princeton) in Fall 2003},
  plclub = {Yes},
  bcp = {Yes},
  keys = {unison}
}
@misc{Pierce:ETAPSTalk2006,
  author = {Benjamin C. Pierce},
  title = {The Weird World of Bi-Directional Programming},
  month = mar,
  year = 2006,
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/lenses-etapsslides.pdf},
  note = {ETAPS invited talk},
  plclub = {Yes},
  bcp = {Yes},
  keys = {harmony}
}
@misc{PierceFSTTCS07,
  author = {Benjamin C. Pierce},
  title = {Adventures in Bi-Directional Programming},
  month = dec,
  year = 2007,
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/boomerang-fsttcs.pdf},
  note = {FSTTCS invited talk},
  plclub = {Yes},
  bcp = {Yes},
  keys = {harmony}
}
@misc{Pierce:MFPSTalk2008,
  author = {Benjamin C. Pierce},
  title = {Types Considered Harmful},
  month = may,
  year = 2008,
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/harmful-mfps.pdf},
  note = {Invited talk at {\em Mathematical Foundations
                  of Programming Semantics (MFPS)}},
  plclub = {Yes},
  bcp = {Yes},
  keys = {typessurveys,contracts}
}
@misc{Pierce:Onward2010,
  author = {Benjamin C. Pierce},
  title = {creativity: sensitivity and surprise},
  month = oct,
  year = 2010,
  slides = {http://www.cis.upenn.edu/~bcpierce/cgi-bin/photos/Onward.pdf},
  note = {Keynote talk at {\em SPLASH / Onward!}},
  plclub = {Yes},
  bcp = {Yes},
  keys = {misc}
}
@misc{Pierce:EPFLTalk2002,
  author = {Benjamin C. Pierce},
  title = {Synchronize globally, compute locally},
  month = jul,
  year = 2002,
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/harmonyslides-epfl.ps},
  note = {Keynote address at {\em Research Day on Global Computing},
                  EFPL, Lausanne},
  plclub = {Yes},
  bcp = {Yes},
  keys = {unison}
}
@techreport{HocusFocusTR2003-old,
  author = {Michael B. Greenwald and Jonathan T. Moore and Benjamin C. Pierce
                  and Alan Schmitt},
  title = {A Language for Bi-Directional Tree Transformations},
  year = 2003,
  type = {Technical Report},
  number = {MS-CIS-03-08},
  institution = {               University of Pennsylvania},
  plclub = {Yes},
  bcp = {Yes},
  note = {Revised April 2004}
}
@techreport{HarmonyOverview,
  author = {Benjamin C. Pierce and Alan Schmitt and Michael B. Greenwald},
  title = {Bringing {H}armony to Optimism:
                  {A} Synchronization Framework for Heterogeneous
                  Tree-Structured Data},
  year = 2003,
  type = {Technical Report},
  number = {MS-CIS-03-42},
  institution = {University of Pennsylvania},
  plclub = {Yes},
  bcp = {Yes},
  tr = {http://www.cis.upenn.edu/~bcpierce/papers/harmony-sync-tr.pdf},
  keys = {unison},
  note = {Superseded by MS-CIS-05-02}
}
@techreport{SYNCTR2005,
  author = {J. Nathan Foster and Michael B. Greenwald and Christian Kirkegaard
                  and Benjamin C. Pierce and Alan Schmitt},
  title = {Schema-Directed Data Synchronization},
  month = mar,
  year = 2005,
  type = {Technical Report},
  number = {MS-CIS-05-02},
  institution = {University of Pennsylvania},
  note = {Supersedes MS-CIS-03-42},
  tr = {http://www.cis.upenn.edu/~bcpierce/papers/sync-tr.pdf},
  bcp = {Yes},
  keys = {unison}
}
@article{SYNC2005,
  author = {J. Nathan Foster and Michael B. Greenwald and Christian Kirkegaard
                  and Benjamin C. Pierce and Alan Schmitt},
  title = {Exploiting Schemas in Data Synchronization},
  journal = {Journal of Computer and System Sciences},
  volume = {73},
  number = {4},
  pages = {669--689},
  year = 2007,
  note = {Extended abstract in
                  {\em Database Programming Languages (DBPL)} 2005},
  tr = {http://www.cis.upenn.edu/~bcpierce/papers/sync-tr.pdf},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/sync-dbpl.pdf},
  slides = {http://www.cis.upenn.edu/~jnfoster/papers/schema-sync-slides.pdf},
  full = {http://www.cis.upenn.edu/~bcpierce/papers/sync-jcss.pdf},
  keys = {harmony},
  plclub = {Yes},
  bcp = {Yes}
}
@unpublished{HocusFocus2003,
  author = {Michael B. Greenwald and Jonathan T. Moore
                  and Benjamin C. Pierce and Alan Schmitt},
  title = {A Language for Bi-Directional Tree Transformations},
  year = 2003,
  institution = {Department of Computer and Information Science, University of Pennsylvania},
  note = {Manuscript; available at \URL{http://www.cis.upenn.edu/~bcpierce/papers/lenses.pdf}},
  plclub = {Yes},
  bcp = {Yes}
}
@inproceedings{SumiiPierce2004,
  author = {Eijiro Sumii and Benjamin C. Pierce},
  title = {A Bisimulation for Dynamic Sealing},
  booktitle = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
                     {L}anguages ({POPL}), Venice, Italy},
  year = {2004},
  plclub = {Yes},
  bcp = {Yes},
  keys = {security},
  conf = {http://www.cis.upenn.edu/~bcpierce/papers/infohide3.pdf},
  note = {Full version in {\em Theoretical Computer Science} 375 (2007), 169--192}
}
@inproceedings{SumiiPierce2005,
  author = {Eijiro Sumii and Benjamin C. Pierce},
  title = {A Bisimulation for Type Abstraction and Recursion},
  booktitle = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
                     {L}anguages ({POPL}), Long Beach, California},
  year = {2005},
  keys = {security},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/infohide5-popl.pdf},
  full = {http://www.cis.upenn.edu/~bcpierce/papers/infohide5-jacm.pdf},
  plclub = {Yes},
  bcp = {Yes},
  note = {Full version in {\em J. ACM}, 54 (5), 2007}
}
@inproceedings{XtaticRuntime,
  title = {{XML} Goes Native: {R}un-time Representations for {Xtatic}},
  author = {Vladimir Gapeyev and Michael Y. Levin
                  and Benjamin C. Pierce and Alan Schmitt},
  year = 2005,
  month = apr,
  booktitle = {14th International Conference on Compiler Construction},
  conf = {http://www.cis.upenn.edu/~bcpierce/papers/xtatic-runtime-CC.pdf},
  tr = {http://www.cis.upenn.edu/~bcpierce/papers/xtatic-runtime-TR.pdf},
  plclub = {Yes},
  bcp = {Yes},
  keys = {xtatic}
}
@inproceedings{XTProgr,
  title = {Statically Typed Document Transformation: {A}n {Xtatic} Experience},
  author = {Vladimir Gapeyev and Fran\c{c}ois Garillot and Benjamin C. Pierce},
  year = 2006,
  month = jan,
  booktitle = {Workshop on Programming Language Technologies for XML (PLAN-X), informal proceedings},
  pdf = {http://www.cis.upenn.edu/~bcpierce/papers/xtprogr-planx.pdf},
  tr = {http://www.cis.upenn.edu/~bcpierce/papers/xtprogr-tr.pdf},
  keys = {xtatic},
  bcp = {Yes},
  plclub = {Yes},
  note = {Available from the Xtatic web site}
}
@inproceedings{XtaticExperience,
  title = {The {Xtatic} Experience},
  author = {Vladimir Gapeyev and Michael Y. Levin
                  and Benjamin C. Pierce and Alan Schmitt},
  booktitle = {Workshop on Programming Language Technologies for XML (PLAN-X)},
  plclub = {Yes},
  bcp = {Yes},
  month = jan,
  year = 2005,
  note = {University of Pennsylvania
                  Technical Report MS-CIS-04-24, Oct 2004},
  keys = {xtatic},
  tr = {http://www.cis.upenn.edu/~bcpierce/papers/xtatic-experience-TR.pdf},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/xtatic-experience-slides.pdf}
}
@techreport{GapeyevPierce2004,
  title = {Paths into Patterns},
  author = {Vladimir Gapeyev and Benjamin C. Pierce},
  year = 2004,
  month = oct,
  type = {Technical Report},
  number = {MS-CIS-04-25},
  institution = {University of Pennsylvania},
  plclub = {Yes},
  bcp = {Yes},
  keys = {xtatic},
  tr = {http://www.cis.upenn.edu/~bcpierce/papers/xtatic-pathambig-TR.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 = {verification},
  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{LevinPierce05,
  title = {Type-based Optimization for Regular Patterns},
  author = {Michael Y. Levin and Benjamin C. Pierce},
  booktitle = {Database Programming Languages (DBPL)},
  year = 2005,
  month = aug,
  bcp = {Yes},
  plclub = {Yes},
  keys = {xtatic},
  tr = {http://www.cis.upenn.edu/~bcpierce/papers/tb-TR.pdf}
}
@unpublished{InCertProposal07,
  title = {Manifest Security},
  author = {Karl Crary and  Robert Harper and Frank Pfenning and
                  Benjamin C. Pierce and Stephanie Weirich and
                  Stephan Zdancewic},
  year = 2007,
  month = jan,
  bcp = {Yes},
  keys = {security},
  plclub = {Yes},
  note = {White paper},
  pdf = {http://www.cis.upenn.edu/~bcpierce/papers/manifestsecurity-whitepaper.pdf}
}
@proceedings{ICFP05,
  title = {International Conference on Functional Programming (ICFP)},
  editor = {Benjamin C. Pierce},
  publisher = {ACM Press},
  year = {2005},
  location = {Tallinn, Estonia, September 2005},
  plclub = {Yes},
  bcp = {Yes}
}
@proceedings{POPL09,
  title = {Principles of Programming Languages (POPL)},
  editor = {Benjamin C. Pierce},
  publisher = {ACM Press},
  year = {2009},
  location = {Savannah, Georgia, January 2009},
  plclub = {Yes},
  bcp = {Yes}
}
@inproceedings{Foster:FTL,
  author = {J. Nathan Foster and Benjamin C. Pierce and Alan Schmitt},
  title = {A Logic Your Typechecker Can Count On: {U}nordered Tree Types in Practice},
  booktitle = {Workshop on Programming Language Technologies for XML (PLAN-X), informal proceedings},
  year = {2007},
  month = jan,
  bcp = {Yes},
  keys = {harmony},
  plclub = {Yes},
  conf = {http://www.cis.upenn.edu/~bcpierce/papers/dtts.pdf},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/dtts-slides.pdf}
}
@misc{Kennedy06,
  author = {Andrew J. Kennedy and Benjamin C. Pierce},
  title = {On Decidability of Nominal Subtyping with Variance},
  year = {2006},
  month = sep,
  bcp = {Yes},
  keys = {oop,subtyping},
  plclub = {Yes},
  note = {FOOL-WOOD '07},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/variance.pdf}
}
@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 = {verification},
  plclub = {Yes},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/binders.pdf}
}
@inproceedings{Greenberg10,
  author = {Michael Greenberg and Benjamin C. Pierce and Stephanie Weirich},
  title = {Contracts Made Manifest},
  year = {2010},
  publisher = {ACM},
  booktitle = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
                     {L}anguages ({POPL}), Madrid, Spain},
  month = jan,
  bcp = {Yes},
  keys = {contracts},
  plclub = {Yes},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/contracts-popl.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 = {verification},
  plclub = {Yes},
  note = {White paper},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/plcurriculum.pdf}
}
@inproceedings{QuotientLenses08,
  author = {J. Nathan Foster and Alexandre Pilkiewicz and Benjamin
                  C. Pierce},
  title = {Quotient Lenses},
  booktitle = {{ACM} {SIGPLAN} {I}nternational {C}onference on {F}unctional {P}rogramming
                    ({ICFP}), Victoria, Canada},
  year = {2008},
  month = sep,
  bcp = {Yes},
  keys = {harmony},
  plclub = {Yes},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/quotient-lenses.pdf}
}
@inproceedings{Boomerang07,
  author = {Aaron Bohannon and J. Nathan Foster and Benjamin C. Pierce and Alexandre Pilkiewicz and Alan Schmitt},
  title = {Boomerang: Resourceful Lenses for String Data},
  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 = {harmony},
  plclub = {Yes},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/boomerang.pdf},
  tr = {http://www.cis.upenn.edu/~bcpierce/papers/boomerang-tr.pdf}
}
@inproceedings{updatable-security-views,
  author = {J. Nathan Foster and Benjamin C. Pierce and Steve Zdancewic},
  title = {Updatable Security Views},
  booktitle = {IEEE Computer Security Foundations Symposium (CSF), Port Jefferson, NY},
  month = jul,
  year = 2009,
  bcp = {yes},
  plclub = {yes},
  conf = {http://www.cis.upenn.edu/~jnfoster/papers/updatable-security-views.pdf}
}
@misc{Pierce:POPL09ChairsReport,
  author = {Benjamin C. Pierce},
  title = {POPL 2009 PC Chair's Report},
  month = jan,
  year = {2009},
  plclub = {Yes},
  bcp = {Yes},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/popl09-chairs-reports.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 = {verification,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 = {verification,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 = {verification,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:SF4,
  author = {Leonidas Lampropoulos and Benjamin C. Pierce},
  title = {{QuickChick}: Property-Based Testing in Coq},
  series = {Software Foundations series, volume 4},
  month = aug,
  year = {2018},
  publisher = {Electronic textbook},
  plclub = {Yes},
  bcp = {Yes},
  keys = {verification,books},
  note = {\URL{http://www.cis.upenn.edu/~bcpierce/sf}},
  ebook = {http://www.cis.upenn.edu/~bcpierce/sf}
}
@misc{Spiders,
  author = {Benjamin C. Pierce and Alessandro Romanel and Daniel Wagner},
  title = {The {Spider Calculus}: Computing in Active Graphs},
  year = {2010},
  plclub = {Yes},
  bcp = {Yes},
  keys = {mobileagents},
  manuscript = {http://www.cis.upenn.edu/~bcpierce/papers/spider_calculus.pdf},
  note = {Manuscript, available from \URL{http://www.cis.upenn.edu/~bcpierce/papers/spider_calculus.pdf}}
}
@inproceedings{DPCS2010,
  author = {Jason Reed and Adam J. Aviv and Daniel
                  Wagner and Andreas Haeberlen and Benjamin C. Pierce and
                  Jonathan M. Smith},
  title = {Differential Privacy for Collaborative Security},
  booktitle = {European Workshop on System Security (EUROSEC)},
  year = {2010},
  month = apr,
  plclub = {Yes},
  bcp = {Yes},
  keys = {security},
  manuscript = {http://www.cis.upenn.edu/~bcpierce/papers/eurosec2010.pdf}
}
@inproceedings{HofmannPierceWagner10:POPL,
  author = {Martin Hofmann and Benjamin C. Pierce and Daniel Wagner},
  title = {Symmetric Lenses},
  year = {2011},
  booktitle = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
                     {L}anguages ({POPL}), Austin, Texas},
  month = jan,
  bcp = {yes},
  plclub = {yes},
  keys = {harmony},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/symmetric.pdf},
  full = {http://www.cis.upenn.edu/~bcpierce/papers/symmetric-full.pdf}
}
@article{HofmannPierceWagner13,
  author = {Martin Hofmann and Benjamin C. Pierce and Daniel Wagner},
  title = {Symmetric Lenses},
  year = {2015},
  journal = {Journal of the ACM},
  note = {To appear; extended abstract in POPL 2011},
  bcp = {yes},
  plclub = {yes},
  keys = {harmony},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/symmetric.pdf}
}
@inproceedings{HofmannPierceWagner12,
  author = {Martin Hofmann and Benjamin C. Pierce and Daniel Wagner},
  title = {Edit Lenses},
  year = {2012},
  booktitle = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
                     {L}anguages ({POPL}), Philadelphia, Pennsylvania},
  month = jan,
  bcp = {yes},
  plclub = {yes},
  keys = {harmony},
  short = {http://dmwit.com/papers/201107EL.pdf},
  slides = {http://dmwit.com/papers/201107EL_slides.pdf}
}
@inproceedings{Matching10,
  author = {Davi M. J. Barbosa and Julien Cretin and Nate Foster
                  and Michael Greenberg and Benjamin C. Pierce},
  title = {Matching Lenses: Alignment and View Update},
  year = {2010},
  month = sep,
  booktitle = {{ACM} {SIGPLAN} {I}nternational {C}onference on {F}unctional {P}rogramming
                    ({ICFP}), Baltimore, Maryland},
  bcp = {yes},
  plclub = {yes},
  keys = {harmony},
  tr = {http://repository.upenn.edu/cis_reports/915/},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/alignment.pdf}
}
@inproceedings{ReedPierce10,
  author = {Jason Reed and Benjamin C. Pierce},
  title = {Distance Makes the Types Grow Stronger:
                  {A} Calculus for Differential Privacy},
  booktitle = {{ACM} {SIGPLAN} {I}nternational {C}onference on {F}unctional {P}rogramming
                    ({ICFP}), Baltimore, Maryland},
  year = {2010},
  month = sep,
  bcp = {yes},
  plclub = {yes},
  keys = {security},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/dp.pdf},
  long = {http://privacy.cis.upenn.edu/papers/metric-pres-tr.pdf}
}
@inproceedings{BohannonPierce10,
  author = {Aaron Bohannon and Benjamin C. Pierce},
  title = {Featherweight {F}irefox:
                  {F}ormalizing the Core of a Web Browser},
  booktitle = {Usenix Conference on Web Application Development (WebApps)},
  year = {2010},
  month = jun,
  bcp = {yes},
  plclub = {yes},
  keys = {security},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/webapps_2010_bohannon_final.pdf}
}
@inproceedings{Bohannon&09,
  author = {Bohannon, Aaron and Pierce, Benjamin C. and Sj\"{o}berg, Vilhelm and Weirich, Stephanie and Zdancewic, Steve},
  title = {Reactive Noninterference},
  booktitle = {CCS '09: Proceedings of the 16th ACM conference on Computer and communications security},
  year = {2009},
  isbn = {978-1-60558-894-0},
  pages = {79--90},
  location = {Chicago, Illinois, USA},
  doi = {http://doi.acm.org/10.1145/1653662.1653673},
  publisher = {ACM},
  address = {New York, NY, USA},
  bcp = {yes},
  plclub = {yes},
  keys = {security}
}
@inproceedings{D'Antoni:2013:SAU:2505351.2505353,
  author = {D'Antoni, Loris and Gaboardi, Marco and Gallego Arias, Emilio Jes\'{u}s and Haeberlen, Andreas and Pierce, Benjamin},
  title = {Sensitivity analysis using type-based constraints},
  booktitle = {Proceedings of the 1st annual workshop on Functional programming concepts in domain-specific languages},
  series = {FPCDSL '13},
  year = {2013},
  isbn = {978-1-4503-2380-2},
  location = {Boston, Massachusetts, USA},
  pages = {43--50},
  numpages = {8},
  url = {http://doi.acm.org/10.1145/2505351.2505353},
  doi = {10.1145/2505351.2505353},
  acmid = {2505353},
  publisher = {ACM},
  address = {New York, NY, USA},
  plclub = {Yes},
  bcp = {Yes},
  keys = {inference}
}
@article{DBLP:journals/jar/PierceW12,
  author = {Benjamin C. Pierce and
                  Stephanie Weirich},
  title = {Preface to Special Issue on the {POPLMark} {C}hallenge},
  journal = {J. Autom. Reasoning},
  volume = {49},
  number = {3},
  year = {2012},
  pages = {301-302},
  ee = {http://dx.doi.org/10.1007/s10817-012-9254-5},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  bcp = {yes},
  plclub = {yes}
}
@article{JAR-POPLMark,
  author = {Benjamin C. Pierce and
                  Stephanie Weirich, editors},
  title = {Special Issue on the POPLMark Challenge},
  journal = {J. Autom. Reasoning},
  volume = {49},
  number = {3},
  year = {2012},
  ee = {http://dx.doi.org/10.1007/s10817-012-9254-5},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  bcp = {yes},
  plclub = {yes}
}
@inproceedings{Haeberlen&11,
  author = {Andreas Haeberlen and Benjamin C. Pierce and
                  Arjun Narayan},
  title = {Differential Privacy Under Fire},
  booktitle = {Proceedings of the 20th USENIX Security Symposium},
  location = {San Francisco, CA},
  month = aug,
  year = {2011},
  bcp = {yes},
  plclub = {yes},
  keys = {security},
  pdf = {http://www.cis.upenn.edu/~ahae/papers/fuzz-sec2011.pdf}
}
@inproceedings{DBLP:conf/esop/BeloGIP11,
  author = {Jo{\~a}o Filipe Belo and
                  Michael Greenberg and
                  Atsushi Igarashi and
                  Benjamin C. Pierce},
  title = {Polymorphic Contracts},
  booktitle = {European Symposium on Programming (ESOP), Saarbr{\"u}cken, Germany},
  year = {2011},
  pages = {18-37},
  ee = {http://dx.doi.org/10.1007/978-3-642-19718-5_2},
  bcp = {Yes},
  plclub = {Yes},
  keys = {contracts},
  crossref = {DBLP:conf/esop/2011},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/esop/2011,
  editor = {Gilles Barthe},
  title = {Programming Languages and Systems - 20th European Symposium
                  on Programming, ESOP 2011, Held as Part of the Joint European
                  Conferences on Theory and Practice of Software, ETAPS 2011,
                  Saarbr{\"u}cken, Germany, March 26-April 3, 2011.
                  Proceedings},
  booktitle = {ESOP},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {6602},
  year = {2011},
  isbn = {978-3-642-19717-8},
  ee = {http://dx.doi.org/10.1007/978-3-642-19718-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@misc{Pierce:PLMW-talk,
  author = {Benjamin C. Pierce},
  title = {Types},
  month = jan,
  year = 2012,
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/PLMW-2012.pdf},
  note = {Invited talk at {\em Programming Languages
                  Mentoring Workshop}},
  keys = {typessurveys},
  plclub = {Yes},
  bcp = {Yes}
}
@misc{CRASH-PLPV-2012.pdf,
  author = {Benjamin C. Pierce},
  title = {Verification Challenges of Pervasive Information Flow},
  month = jan,
  year = 2012,
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/CRASH-PLPV-2012.pdf},
  note = {Invited talk at {\em Programming Languages
                  Meets Program Verification} workshop (PLPV)},
  plclub = {Yes},
  bcp = {Yes},
  keys = {security}
}
@misc{TypesALaMilner,
  author = {Benjamin C. Pierce},
  title = {Types {\` a} la {M}ilner},
  month = apr,
  year = 2012,
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/TypesALaMilner.pdf},
  note = {Invited talk at {\em Milner Symposium}},
  keys = {typessurveys},
  plclub = {Yes},
  bcp = {Yes}
}
@misc{TypesALaMilner-ETE,
  author = {Benjamin C. Pierce},
  title = {Types {\` a} la {M}ilner},
  month = apr,
  year = 2012,
  video = {http://youtu.be/carP8i6YSZs},
  note = {Talk at {\em Philly Emerging Technologies Conference}},
  keys = {typessurveys},
  plclub = {Yes},
  bcp = {Yes}
}
@misc{Pierce-PODS12,
  author = {Benjamin C. Pierce},
  title = {Linguistic Foundations for Bidirectional Transformations},
  month = may,
  year = 2012,
  note = {Invited tutorial at {\em Principles of Database Systems (PODS)}},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/PODStutorial2012.pdf},
  keys = {harmony},
  plclub = {Yes},
  bcp = {Yes}
}
@inproceedings{DFuzz,
  author = {Marco Gaboardi and Andreas Haeberlen and Justin Hsu and
                  Arjun Narayan and Benjamin C. Pierce},
  title = {Linear Dependent Types for Differential Privacy},
  year = {2013},
  booktitle = {{ACM} {SIGPLAN--SIGACT} {S}ymposium on {P}rinciples of {P}rogramming
                     {L}anguages ({POPL}), Rome, Italy},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/dfuzz2013.pdf},
  month = jan,
  bcp = {yes},
  plclub = {yes},
  keys = {security}
}
@misc{DIMACS-2012,
  author = {Benjamin C. Pierce},
  title = {Differential Privacy in the Programming Languages Community},
  month = oct,
  year = 2012,
  video = {http://www.youtube.com/watch/ci2aueqZ6CU},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/DIMACS-DP-PL.pdf},
  note = {Invited tutorial at {\em DIMACS Workshop on Recent Work
                  on Differential Privacy across Computer Science}},
  keys = {security},
  plclub = {Yes},
  bcp = {Yes}
}
@inproceedings{GenLabels,
  title = {A Theory of Information-Flow Labels},
  author = {Beno\^it Montagu and
    Benjamin C. Pierce and
    Randy Pollack},
  month = jun,
  year = {2013},
  location = {New Orleans, Louisiana, USA},
  booktitle = {Proceedings of the 2013 IEEE Computer Security Foundations Symposium},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/csf2013.pdf},
  coq = {http://www.cis.upenn.edu/~bcpierce/papers/label_algebras.tar.gz},
  plclub = {Yes},
  keys = {security},
  bcp = {Yes}
}
@inproceedings{Exceptional,
  author = {C\u{a}t\u{a}lin Hri\c{t}cu and
            Michael Greenberg and
            Ben Karel and
            Benjamin C. Pierce and
            Greg Morrisett},
  title = {All Your {IFCException} Are Belong To Us},
  booktitle = {34th IEEE Symposium on Security and Privacy (Oakland)},
  year = {2013},
  month = may,
  plclub = {Yes},
  bcp = {Yes},
  keys = {security},
  short = {http://www.crash-safe.org/node/23}
}
@inproceedings{TestingNI:ICFP,
  author = {C\u{a}t\u{a}lin Hri\c{t}cu and
                  John Hughes and
                  Benjamin C. Pierce and
                  Antal Spector-Zabusky and
                  Dimitrios Vytiniotis and
                  Arthur {Azevedo de Amorim} and
                  Leonidas Lampropoulos},
  title = {Testing Noninterference, Quickly},
  booktitle = {18th ACM SIGPLAN International
                  Conference on Functional Programming (ICFP)},
  shortbooktitle = {ICFP},
  year = {2013},
  month = sep,
  url = {http://www.crash-safe.org/node/24},
  bcp = {yes},
  plclub = {yes},
  keys = {verification,security},
  note = {Full version in Journal of Functional Programming, special issue for ICFP 2013, 26:e4 (62 pages), April 2016. Technical Report available as arXiv:1409.0393.}
}
@inproceedings{ieee_hst2013:SAFE,
  author = {Silviu Chiricescu and Andr\'{e} DeHon and
                  Delphine Demange and Suraj Iyer and Aleksey Kliger and Greg Morrisett
                  and Benjamin C. Pierce and Howard Reubenstein and Jonathan M. Smith
                  and Gregory T. Sullivan and Arun Thomas and Jesse Tov and Christopher M. White
                  and David Wittenberg},
  title = {SAFE: A Clean-Slate Architecture for Secure Systems},
  booktitle = {Proceedings of the {IEEE} International Conference on
                  Technologies for Homeland Security},
  year = {2013},
  month = nov,
  bcp = {yes},
  plclub = {yes},
  keys = {security}
}
@inproceedings{pump_hasp2014,
  author = {Udit Dhawan and Nikos Vasilakis and Raphael Rubin
                  and Silviu Chiricescu and Jonathan M. Smith
and Thomas F. Knight and Benjamin C. Pierce and Andr\'e DeHon},
  title = {{PUMP -- A Programmable Unit for Metadata Processing}},
  booktitle = {Proceedings of the 3rd International Workshop on Hardware and Architectural Support for Security and Privacy},
  series = {HASP '14},
  year = {2014},
  isbn = {},
  location = {Minneapolis, USA},
  pages = {},
  articleno = {},
  numpages = {8},
  url = {http://www.crash-safe.org/node/32},
  doi = {},
  acmid = {},
  publisher = {ACM},
  address = {New York, NY, USA},
  bcp = {yes},
  plclub = {yes},
  keys = {security}
}
@inproceedings{interlocks_ahns2012,
  author = {
  Udit Dhawan and
  Albert Kwon and
  Edin Kadric and
  C\u{a}t\u{a}lin Hri\c{t}cu and
  Benjamin C. Pierce and
  Jonathan M. Smith and
  Gregory Malecha and
  Greg Morrisett and
  Thomas F. {Knight, Jr.} and
  Andrew Sutherland and
  Tom Hawkins and
  Amanda Zyxnfryx and
  David Wittenberg and
  Peter Trei and
  Sumit Ray and
  Greg Sullivan and
  Andr\'e DeHon
  },
  title = {Hardware Support for Safety Interlocks and Introspection},
  url = {http://www.crash-safe.org/sites/default/files/interlocks_ahns2012.pdf},
  month = sep,
  year = 2012,
  booktitle = {SASO Workshop on Adaptive Host and  Network Security},
  bcp = {yes},
  plclub = {yes},
  keys = {harmony}
}
@inproceedings{HofmannPierceWagner13a,
  author = {Martin Hofmann and Benjamin C. Pierce and Daniel Wagner},
  title = {Edit languages for information trees},
  year = {2013},
  booktitle = {Second International Workshop on Bidirectional Transformations (BX)},
  month = apr,
  bcp = {yes},
  plclub = {yes},
  keys = {harmony}
}
@misc{Pierce:CSFTalk2013,
  author = {Benjamin C. Pierce},
  title = {The {SAFE} Machine: {A}n Architecture for
                  Pervasive Information Flow},
  month = jun,
  year = 2013,
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/csf-2013-pierce.pdf},
  note = {Invited talk at {\em Computer Security
                  Foundations Symposium (CSF)}},
  plclub = {Yes},
  bcp = {Yes},
  keys = {security}
}
@misc{Pierce:SPLASHTalk2016,
  author = {Benjamin C. Pierce},
  title = {The Science of Deep Specification},
  month = nov,
  year = 2016,
  note = {Invited keynote at {\em SPLASH / OOPSLA}},
  plclub = {Yes},
  bcp = {Yes},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/deepspec-splash2016.pdf},
  video = {https://www.youtube.com/watch?v=IPNdsnRWBkk&t=5s},
  keys = {verification}
}
@misc{Pierce:ETAPSTalk2018,
  author = {Benjamin C. Pierce},
  title = {The Science of Deep Specification},
  month = apr,
  year = 2018,
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/pierce-etaps2018.pdf},
  note = {Invited keynote at {\em ETAPS / POST}},
  plclub = {Yes},
  bcp = {Yes},
  video = {https://www.etaps.org/index.php/2018/invited-speakers},
  keys = {verification}
}
@inproceedings{Epsilon2014,
  title = {Differential Privacy: An Economic Method for Choosing
                  Epsilon},
  author = {Justin Hsu and Marco Gaboardi and
                  Andreas Haeberlen and Sanjeev Khanna and
                  Arjun Narayan and Benjamin C. Pierce and Aaron Roth},
  booktitle = {Computer Security
                  Foundations Symposium (CSF)},
  year = 2014,
  url = {http://www.cis.upenn.edu/~bcpierce/papers/epsilon-csf.pdf},
  plclub = {Yes},
  bcp = {Yes},
  keys = {security}
}
@inproceedings{PicoCoq2013:POPL,
  title = {A Verified Information-Flow Architecture},
  author = {
    Arthur {Azevedo de Amorim} and
    Nathan Collins and
    Andr\'e DeHon and
    Delphine Demange and
    C\u{a}t\u{a}lin Hri\c{t}cu and
    David Pichardie and
    Benjamin C. Pierce and
    Randy Pollack and
    Andrew Tolmach
  },
  booktitle = {Proceedings of the 41st Symposium on Principles of Programming Languages},
  series = {POPL},
  month = jan,
  year = 2014,
  url = {http://www.cis.upenn.edu/~bcpierce/papers/verified-ifc.pdf},
  full = {http://arxiv.org/abs/1509.06503},
  plclub = {Yes},
  bcp = {Yes},
  keys = {security},
  note = {Full version in Journal of Computer Security, Special Issue on Verified Information Flow Security, Dec 2016}
}
@inproceedings{SAFEPLOS11:PreliminaryDesign,
  author = {
  Andr\'{e} DeHon and
  Ben Karel and
  Thomas F. {Knight, Jr.} and
  Gregory Malecha and
  Beno\^{i}t Montagu and
  Robin Morisset and
  Greg Morrisett and
  Benjamin C. Pierce and
  Randy Pollack and
  Sumit Ray and
  Olin Shivers and
  Jonathan M. Smith and
  Gregory Sullivan
  },
  title = {Preliminary Design of the {SAFE} Platform},
  month = oct,
  year = 2011,
  url = {http://www.crash-safe.org/sites/default/files/plos11-final_0.pdf},
  booktitle = {6th Workshop on Programming
  Languages and Operating Systems},
  series = {PLOS},
  shortbooktitle = {PLOS},
  location = {Cascais, Portugal},
  plclub = {Yes},
  bcp = {Yes},
  keys = {security}
}
@misc{Pierce:PiPTalk2014,
  author = {Benjamin C. Pierce},
  title = {Principles, Meet Practice: An Early Retrospective on SAFE},
  month = jan,
  year = 2014,
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/safe-PiP-140126.pdf},
  note = {Talk at {\em Principles in Practice Workshop (PiP)}},
  plclub = {Yes},
  bcp = {Yes},
  keys = {security}
}
@misc{Pierce:HCSSTalk2014,
  author = {Benjamin C. Pierce},
  title = {Programmable Hardware Support for Ubiquitous Micro-Policy
  Enforcement},
  month = may,
  year = 2014,
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/hcss2014-slides.pdf},
  note = {Talk at {\em High-Confidence Software Systems}},
  plclub = {Yes},
  bcp = {Yes},
  keys = {security}
}
@misc{Pierce:LukeInterview,
  author = {Benjamin C. Pierce},
  title = {{Interview with Luke Muehlhauser on Clean-Slate Security Architectures for Machine Intelligence Research Institute blog}},
  month = may,
  year = 2014,
  transcript = {http://intelligence.org/2014/05/11/benjamin-pierce/},
  plclub = {Yes},
  bcp = {Yes},
  keys = {security}
}
@inproceedings{pump_oakland2015,
  author = {Arthur {Azevedo de Amorim} and
                  Maxime D\'en\`es and
                  Nick Giannarakis and
                  C\u{a}t\u{a}lin Hri\c{t}cu and
                  Benjamin C. Pierce and
                  Antal Spector-Zabusky and
                  Andrew Tolmach},
  title = {Micro-Policies: Formally Verified, Tag-Based Security Monitors},
  booktitle = {36th IEEE Symposium on Security and Privacy (Oakland S\&P)},
  year = {2015},
  month = may,
  short = {http://prosecco.gforge.inria.fr/personal/hritcu/publications/micro-policies.pdf},
  fullurl = {https://www.cis.upenn.edu/~aarthur/micro-policies-full.pdf},
  slides = {http://www.seas.upenn.edu/~aarthur/micro-policies-slides.pdf},
  publisher = {IEEE},
  acceptance = {55/420=0.13},
  plclub = {Yes},
  bcp = {Yes},
  keys = {security}
}
@phdthesis{WagnerThesis,
  author = {Daniel Wagner},
  title = {Symmetric Edit Lenses:
                 A New Foundation for Bidirectional Languages},
  school = {University of Pennsylvania},
  year = {2014},
  bcp = {Yes},
  keys = {harmony},
  plclub = {Yes},
  pdf = {http://www.cis.upenn.edu/~bcpierce/papers/wagner-thesis.pdf}
}
@article{DBLP:journals/entcs/BrookesPPS13,
  author = {Stephen Brookes and
               Benjamin C. Pierce and
               Gordon D. Plotkin and
               Dana S. Scott},
  title = {Dedication to {John Reynolds}},
  journal = {Electr. Notes Theor. Comput. Sci.},
  volume = {298},
  pages = {3--5},
  year = {2013},
  url = {http://dx.doi.org/10.1016/j.entcs.2013.09.004},
  doi = {10.1016/j.entcs.2013.09.004},
  timestamp = {Fri, 03 Jan 2014 15:10:40 +0100},
  biburl = {http://dblp.uni-trier.de/rec/bib/journals/entcs/BrookesPPS13},
  bibsource = {dblp computer science bibliography, http://dblp.org},
  plclub = {Yes},
  bcp = {Yes},
  note = {Special Issue: Proceedings of the 29th Conference on Mathematical Foundations of Programming Semantics (MFPS)}
}
@inproceedings{Denes:VSL2014,
  author = {Maxime D\'en\`es and Catalin Hritcu and Leonidas Lampropoulos and Zoe Paraskevopoulou and Benjamin C. Pierce},
  title = {{QuickChick}: {P}roperty-Based Testing for {C}oq (abstract)},
  booktitle = {VSL},
  url = {http://www.easychair.org/smart-program/VSL2014/index.html},
  year = 2014,
  plclub = {Yes},
  bcp = {Yes},
  keys = {verification}
}
@inproceedings{Paraskevopoulou:ITP2015,
  author = {Zoe Paraskevopoulou and
                  C\u{a}t\u{a}lin Hri\c{t}cu and
                  Maxime D\'en\`es and
                  Leonidas Lampropoulos and
                  Benjamin C. Pierce},
  title = {Foundational Property-Based Testing},
  booktitle = {International Conference
                  on Interactive Theorem Proving (ITP)},
  year = 2015,
  plclub = {Yes},
  bcp = {Yes},
  keys = {verification}
}
@misc{pump:asplos2015,
  author = {Udit Dhawan and
          C\u{a}t\u{a}lin Hri\c{t}cu and
          Rafi Rubin and
          Nikos Vasilakis and
          Silviu Chiricescu and
          Jonathan M. Smith and
          Thomas F. {Knight, Jr.} and
          Benjamin C. Pierce and
          Andr\'{e} DeHon},
  title = {Architectural Support for Software-Defined Metadata Processing},
  howpublished = asplos,
  year = {2015},
  url = {http://ic.ese.upenn.edu/abstracts/sdmp_asplos2015.html},
  plclub = {Yes},
  bcp = {Yes},
  keys = {security}
}
@misc{Pierce:MicroPoliciesTalk2014,
  author = {Benjamin C. Pierce},
  title = {Micro-Policies: A Framework for Tag-Based Security Monitors},
  month = dec,
  year = 2014,
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/upolicies-201412.pdf},
  note = {Distinguished Lecture at University of Minnesota},
  plclub = {Yes},
  bcp = {Yes},
  keys = {security}
}
@inproceedings{beyond-good-and-evil,
  author = {Yannis Juglaret and
           C\u{a}t\u{a}lin Hri\c{t}cu and
           Arthur {Azevedo de Amorim} and
           Boris Eng and
           Benjamin C. Pierce},
  title = {Beyond Good and Evil: Formalizing the Security Guarantees
                 of Compartmentalizing Compilation},
  booktitle = {29th IEEE Symposium on Computer Security Foundations (CSF)},
  shortbooktitle = {CSF},
  year = {2016},
  month = jul,
  publisher = {IEEE Computer Society Press},
  url = {http://arxiv.org/abs/1602.04503},
  acceptance = {31/87=0.36},
  note = {arXiv:1602.04503},
  plclub = {Yes},
  bcp = {Yes},
  keys = {security}
}
@article{Murawski:2016:2893582,
  title = {Programming language techniques for differential privacy},
  author = {Barthe, Gilles and
                Gaboardi, Marco and
                Hsu, Justin and
                Pierce, Benjamin C},
  pages = {34--53},
  editor = {Murawski, Andrzej},
  journal = {ACM SIGLOG News},
  month = jan,
  year = {2016},
  volume = {3},
  number = {1},
  publisher = {ACM},
  address = {New York, NY, USA},
  url = {http://siglog.hosting.acm.org/wp-content/uploads/2016/01/siglog_news_7.pdf},
  bcp = {Yes},
  plclub = {Yes},
  bcp = {Yes},
  keys = {security}
}
@misc{Pierce:DeepSpecHCSS2016,
  author = {Benjamin C. Pierce},
  title = {The Science of Deep Specification},
  month = may,
  year = 2016,
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/deepspec-hcss2016-slides.pdf},
  plclub = {Yes},
  bcp = {Yes},
  keys = {verification},
  note = {High-Confidence Software Systems (HCSS)}
}
@article{WinogradCort2017,
  author = {Daniel Winograd{-}Cort and
               Andreas Haeberlen and
               Aaron Roth and
               Benjamin C. Pierce},
  title = {A framework for adaptive differential privacy},
  journal = {{PACMPL}},
  volume = {1},
  number = {{ICFP}},
  pages = {10:1--10:29},
  year = {2017},
  url = {http://doi.acm.org/10.1145/3110254},
  doi = {10.1145/3110254},
  timestamp = {Tue, 12 Sep 2017 16:16:51 +0200},
  biburl = {https://dblp.org/rec/bib/journals/pacmpl/Winograd-CortHR17},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  plclub = {Yes},
  bcp = {Yes}
}
@incollection{beginners-luck,
  author = {Leonidas Lampropoulos and
                  Diane Gallois-Wong and
                  C\u{a}t\u{a}lin Hri\c{t}cu and
                  John Hughes and
                  Benjamin C. Pierce and
                  {Li-yao} Xia},
  title = {Beginner's {Luck}: {A} Language for Random Generators},
  booktitle = {Foundations of Programming and Software systems: Probabilistic Programming},
  editor = {Gilles Barthe and Joost-Pieter Katoen and Alexandra Silva},
  year = {2020},
  url = {https://arxiv.org/abs/1607.05443},
  plclub = {Yes},
  bcp = {Yes},
  keys = {verification},
  note = {An earlier version appeared in ACM SIGPLAN Symposium on Principles of Programming
                  Languages (POPL), Jan 2017}
}
@inproceedings{beginners-luck:popl,
  author = {Leonidas Lampropoulos and
                  Diane Gallois-Wong and
                  C\u{a}t\u{a}lin Hri\c{t}cu and
                  John Hughes and
                  Benjamin C. Pierce and
                  {Li-yao} Xia},
  title = {Beginner's {Luck}: A Language for Random Generators},
  booktitle = {44th ACM SIGPLAN Symposium on Principles of Programming
                  Languages (POPL)},
  year = {2017},
  month = jan,
  url = {https://arxiv.org/abs/1607.05443},
  acceptance = {64/279=0.23},
  plclub = {Yes},
  bcp = {Yes},
  keys = {verification}
}
@misc{Pierce:PLMWTalk2017,
  author = {Benjamin C. Pierce},
  title = {The Curse of Knowledge},
  month = jan,
  year = 2017,
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/plmw2017-curse-of-knowledge.pdf},
  note = {Talk at Programming Languages Mentoring Workshop (PLMW)},
  plclub = {Yes},
  bcp = {Yes},
  keys = {misc}
}
@misc{Pierce:PLMWTalk2018,
  author = {Benjamin C. Pierce},
  title = {The Curse of Knowledge},
  month = jan,
  year = 2018,
  note = {Talk at Programming Languages Mentoring Workshop (PLMW)},
  plclub = {Yes},
  bcp = {Yes},
  keys = {misc}
}
@inproceedings{AzevedoDeAmorim17,
  author = {Arthur Azevedo de Amorim and
               Catalin Hritcu and
               Benjamin C. Pierce},
  editor = {Lujo Bauer and
               Ralf K{\"{u}}sters},
  title = {The Meaning of Memory Safety},
  booktitle = {Principles of Security and Trust - 7th International Conference, {POST}
               2018, Held as Part of the European Joint Conferences on Theory and
               Practice of Software, {ETAPS} 2018, Thessaloniki, Greece, April 14-20,
               2018, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {10804},
  pages = {79--105},
  publisher = {Springer},
  year = {2018},
  url = {https://doi.org/10.1007/978-3-319-89722-6\_4},
  doi = {10.1007/978-3-319-89722-6\_4},
  timestamp = {Fri, 31 Jan 2020 21:32:30 +0100},
  biburl = {https://dblp.org/rec/conf/post/AmorimHP18.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  plclub = {Yes},
  bcp = {Yes},
  keys = {verification}
}
@inproceedings{AzevedoDeAmorim17old,
  author = {Arthur {Azevedo de Amorim} and
                  C\u{a}t\u{a}lin Hri\c{t}cu and
                  Benjamin C. Pierce},
  title = {The Meaning of Memory Safety},
  booktitle = {ACM Conference on Computer and Communications Security (CCS)},
  year = 2017,
  plclub = {Yes},
  bcp = {Yes},
  keys = {verification},
  note = {Under submission}
}
@misc{Pierce:ReleaseInterview,
  author = {Benjamin C. Pierce},
  title = {{Interview with Tijs van der Storm on The Science of Deep Specification for release.nl magazine}},
  month = nov,
  year = 2016,
  transcript = {http://release.nl/293/video.html?video=775966},
  plclub = {Yes},
  bcp = {Yes},
  keys = {security,verification}
}
@misc{Pierce:OmegaTauInterview,
  author = {Benjamin C. Pierce},
  title = {{Interview with Markus V\"olter on The Science of Deep Specification for Omega Tau podcast}},
  month = nov,
  year = 2016,
  transcript = {http://omegataupodcast.net/243-formal-specification-and-proof/},
  plclub = {Yes},
  bcp = {Yes},
  keys = {security,verification}
}
@misc{Pierce:NSFtalk2017,
  author = {Benjamin C. Pierce},
  title = {The Science of Deep Specification},
  month = sep,
  year = 2017,
  note = {WATCH lecture at NSF},
  plclub = {Yes},
  bcp = {Yes},
  keys = {verification}
}
@misc{Pierce:DeepWeb-dsw2018,
  author = {Benjamin C. Pierce},
  title = {Specifying the {DeepSpec Web Server}},
  month = jun,
  year = 2018,
  note = {Talk at {\it DeepSpec} workshop},
  plclub = {Yes},
  bcp = {Yes},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/DeepWeb-dsw2018.pdf},
  keys = {verification}
}
@misc{Pierce:DeepWeb-dsw2019,
  author = {Benjamin C. Pierce},
  title = {The Science of Deep Specification},
  month = jun,
  year = 2019,
  note = {Opening talk at {\it DeepSpec} workshop},
  plclub = {Yes},
  bcp = {Yes},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/DeepSpec-workshop-2019-Intro.pdf},
  keys = {verification}
}
@article{Appel20160331,
  author = {Appel, Andrew W. and Beringer, Lennart and Chlipala, Adam and Pierce, Benjamin C. and Shao, Zhong and Weirich, Stephanie and Zdancewic, Steve},
  title = {Position paper: {T}he science of deep specification},
  volume = {375},
  number = {2104},
  year = {2017},
  doi = {10.1098/rsta.2016.0331},
  publisher = {The Royal Society},
  abstract = {We introduce our efforts within the project
                  {\textquoteleft}The science of deep
                  specification{\textquoteright} to work out the key
                  formal underpinnings of industrial-scale formal
                  specifications of software and hardware components,
                  anticipating a world where large verified systems
                  are routinely built out of smaller verified
                  components that are also used by many other
                  projects. We identify an important class of
                  specification that has already been used in a few
                  experiments that connect strong
                  component-correctness theorems across the work of
                  different teams. To help popularize the unique
                  advantages of that style, we dub it deep
                  specification, and we say that it encompasses
                  specifications that are rich, two-sided, formal and
                  live (terms that we define in the article). Our core
                  team is developing a proof-of-concept system (based
                  on the Coq proof assistant) whose specification and
                  verification work is divided across largely
                  decoupled subteams at our four institutions,
                  encompassing hardware microarchitecture, compilers,
                  operating systems and applications, along with
                  cross-cutting principles and tools for effective
                  specification. We also aim to catalyse interest in
                  the approach, not just by basic researchers but also
                  by users in industry. This article is part of the
                  themed issue {\textquoteleft}Verified trustworthy
                  software systems{\textquoteright}.},
  issn = {1364-503X},
  url = {http://rsta.royalsocietypublishing.org/content/375/2104/20160331},
  eprint = {http://rsta.royalsocietypublishing.org/content/375/2104/20160331.full.pdf},
  journal = {Philosophical Transactions of the Royal Society of London A: Mathematical, Physical and Engineering Sciences},
  plclub = {Yes},
  bcp = {Yes},
  keys = {security,verification}
}
@article{DBLP:journals/corr/ChongGDMPSSZ16,
  author = {Stephen Chong and
                  Joshua Guttman and
                  Anupam Datta and
                  Andrew C. Myers and
                  Benjamin Pierce and
                  Patrick Schaumont and
                  Tim Sherwood and
                  Nickolai Zeldovich},
  title = {Report on the {NSF} Workshop on Formal Methods for Security},
  journal = {CoRR},
  volume = {abs/1608.00678},
  year = {2016},
  url = {http://arxiv.org/abs/1608.00678},
  timestamp = {Mon, 24 Oct 2016 15:22:59 +0200},
  biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/ChongGDMPSSZ16},
  bibsource = {dblp computer science bibliography, http://dblp.org},
  plclub = {Yes},
  bcp = {Yes}
}
@article{DBLP:journals/corr/ChongGDMPSSZ16:again,
  author = {Stephen Chong and
               Joshua Guttman and
               Anupam Datta and
               Andrew C. Myers and
               Benjamin Pierce and
               Patrick Schaumont and
               Tim Sherwood and
               Nickolai Zeldovich},
  title = {Report on the {NSF} Workshop on Formal Methods for Security},
  journal = {CoRR},
  volume = {abs/1608.00678},
  year = {2016},
  url = {http://arxiv.org/abs/1608.00678},
  timestamp = {Mon, 24 Oct 2016 15:22:59 +0200},
  biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/ChongGDMPSSZ16},
  bibsource = {dblp computer science bibliography, http://dblp.org},
  plclub = {Yes},
  bcp = {Yes}
}
@article{Miltner&18,
  author = {Anders Miltner and
               Kathleen Fisher and
               Benjamin C. Pierce and
               David Walker and
               Steve Zdancewic},
  title = {Synthesizing bijective lenses},
  journal = {{PACMPL}},
  volume = {2},
  number = {{POPL}},
  pages = {1:1--1:30},
  year = {2018},
  url = {http://doi.acm.org/10.1145/3158089},
  doi = {10.1145/3158089},
  timestamp = {Fri, 05 Jan 2018 12:57:30 +0100},
  biburl = {https://dblp.org/rec/bib/journals/pacmpl/MiltnerFPWZ18},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  plclub = {Yes},
  bcp = {Yes},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/synth-bij-lenses.pdf},
  keys = {harmony}
}
@article{Lampropoulos&18,
  author = {Leonidas Lampropoulos and
               Zoe Paraskevopoulou and
               Benjamin C. Pierce},
  title = {Generating good generators for inductive relations},
  journal = {{PACMPL}},
  volume = {2},
  number = {{POPL}},
  pages = {45:1--45:30},
  year = {2018},
  url = {http://doi.acm.org/10.1145/3158133},
  doi = {10.1145/3158133},
  timestamp = {Fri, 05 Jan 2018 12:57:30 +0100},
  biburl = {https://dblp.org/rec/bib/journals/pacmpl/LampropoulosPP18},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  plclub = {Yes},
  bcp = {Yes},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/generating-good.pdf},
  keys = {verification}
}
@misc{Pierce:ClimateCommitteReport,
  author = {Michael W. Hicks and Crista Lopes and Benjamin C. Pierce},
  title = {Engaging with Climate Change:
                  Some Possible Steps for SIGPLAN
                  (Preliminary Report of the SIGPLAN Climate Committee, Version 1.2)},
  month = jun,
  year = 2018,
  url = {http://www.cis.upenn.edu/~bcpierce/papers/sigplan-climate-report.pdf},
  plclub = {Yes},
  bcp = {Yes},
  keys = {misc,climate}
}
@misc{Pierce:ClimateCommitteReportAtPLDI18,
  author = {Michael W. Hicks and Crista Lopes and Jens Palsberg
                  and Benjamin C. Pierce},
  title = {{SIGPLAN} and Climate Change: {A} report from {SIGPLAN}'s
                  ad hoc committee on climate change},
  month = jun,
  year = 2018,
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/PLDI2018-townhall-slides.pdf},
  keynote = {http://www.cis.upenn.edu/~bcpierce/papers/PLDI2018-townhall-slides.key},
  video = {http://www.cis.upenn.edu/~bcpierce/papers/PLDI2018-townhall.mov},
  plclub = {Yes},
  bcp = {Yes},
  keys = {misc,climate}
}
@misc{Pierce:ClimateCommitteReportAtICFP18,
  author = {Michael W. Hicks and Crista Lopes and Jens Palsberg
                  and Benjamin C. Pierce},
  title = {{SIGPLAN} and Climate Change: {A} report from the {SIGPLAN}
                  committee on climate change},
  month = sep,
  year = 2018,
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/ICFP2018-slides.pdf},
  keynote = {http://www.cis.upenn.edu/~bcpierce/papers/ICFP2018-slides.key},
  video = {XXXXX},
  plclub = {Yes},
  bcp = {Yes},
  keys = {misc,climate}
}
@misc{CarbonOFfsetReport,
  author = {Richard Kim and Benjamin C. Pierce},
  title = {Carbon Offsets: An Overview for Scientific Societies},
  month = jun,
  year = 2018,
  url = {http://www.cis.upenn.edu/~bcpierce/papers/carbon-offsets.pdf},
  note = {Version 1.2},
  plclub = {Yes},
  bcp = {Yes},
  keys = {misc,climate}
}
@inproceedings{DBLP:conf/eurosp/SchoepeBPS16,
  author = {Daniel Schoepe and
               Musard Balliu and
               Benjamin C. Pierce and
               Andrei Sabelfeld},
  title = {Explicit Secrecy: {A} Policy for Taint Tracking},
  booktitle = {{IEEE} European Symposium on Security and Privacy, EuroS{\&}P
               2016, Saarbr{\"{u}}cken, Germany, March 21-24, 2016},
  pages = {15--30},
  year = {2016},
  crossref = {DBLP:conf/eurosp/2016},
  url = {https://doi.org/10.1109/EuroSP.2016.14},
  doi = {10.1109/EuroSP.2016.14},
  timestamp = {Wed, 24 May 2017 08:27:42 +0200},
  biburl = {http://dblp.org/rec/bib/conf/eurosp/SchoepeBPS16},
  bibsource = {dblp computer science bibliography, http://dblp.org},
  plclub = {Yes},
  bcp = {Yes},
  keys = {security}
}
@proceedings{DBLP:conf/eurosp/2016,
  title = {{IEEE} European Symposium on Security and Privacy, EuroS{\&}P
               2016, Saarbr{\"{u}}cken, Germany, March 21-24, 2016},
  publisher = {{IEEE}},
  year = {2016},
  url = {http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=7467055},
  isbn = {978-1-5090-1751-5},
  timestamp = {Sun, 05 Jun 2016 10:00:11 +0200},
  biburl = {http://dblp.org/rec/bib/conf/eurosp/2016},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@misc{Yang17,
  author = {Jean Yang},
  title = {People of {P}rogramming {L}anguages: {I}nterview with
                  {B}enjamin {P}ierce},
  month = dec,
  year = 2017,
  url = {http://www.cs.cmu.edu/~popl-interviews/pierce.html},
  plclub = {Yes},
  bcp = {Yes},
  keys = {misc}
}
@inproceedings{abate2018good,
  title = {When good components go bad: Formally secure compilation despite dynamic compromise},
  author = {Abate, Carmine and {Azevedo de Amorim}, Arthur and Blanco, Roberto and Evans, Ana Nora and Fachini, Guglielmo and Hritcu, Catalin and Laurent, Th{\'e}o and Pierce, Benjamin C and Stronati, Marco and Tolmach, Andrew},
  booktitle = {Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security},
  pages = {1351--1368},
  year = {2018},
  organization = {ACM},
  plclub = {Yes},
  bcp = {Yes},
  keys = {security}
}
@inproceedings{DBLP:conf/post/AmorimHP18,
  author = {Arthur {Azevedo de Amorim} and
               Catalin Hritcu and
               Benjamin C. Pierce},
  title = {The Meaning of Memory Safety},
  booktitle = {Principles of Security and Trust - 7th International Conference, {POST}
               2018, Held as Part of the European Joint Conferences on Theory and
               Practice of Software, {ETAPS} 2018, Thessaloniki, Greece, April 14-20,
               2018, Proceedings},
  pages = {79--105},
  year = {2018},
  crossref = {DBLP:conf/post/2018},
  url = {https://doi.org/10.1007/978-3-319-89722-6_4},
  doi = {10.1007/978-3-319-89722-6_4},
  timestamp = {Mon, 16 Apr 2018 13:28:26 +0200},
  biburl = {https://dblp.org/rec/bib/conf/post/AmorimHP18},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  plclub = {Yes},
  bcp = {Yes},
  keys = {security}
}
@proceedings{DBLP:conf/post/2018,
  editor = {Lujo Bauer and
               Ralf K{\"{u}}sters},
  title = {Principles of Security and Trust - 7th International Conference, {POST}
               2018, Held as Part of the European Joint Conferences on Theory and
               Practice of Software, {ETAPS} 2018, Thessaloniki, Greece, April 14-20,
               2018, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {10804},
  publisher = {Springer},
  year = {2018},
  url = {https://doi.org/10.1007/978-3-319-89722-6},
  doi = {10.1007/978-3-319-89722-6},
  isbn = {978-3-319-89721-9},
  timestamp = {Mon, 16 Apr 2018 13:26:44 +0200},
  biburl = {https://dblp.org/rec/bib/conf/post/2018},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}
@misc{Pierce:MartinHofmannMemorial,
  author = {Benjamin C. Pierce},
  title = {In Memoriam {M}artin {H}ofmann},
  month = jul,
  year = 2018,
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/MartinHofmannMemorial.pdf},
  keynote = {http://www.cis.upenn.edu/~bcpierce/papers/MartinHofmannMemorial.key},
  video = {https://www.youtube.com/watch?v=WpWt40l_uDk},
  plclub = {Yes},
  bcp = {Yes},
  keys = {misc},
  note = {The Apple Keynote version includes the music from the
                  presentation, plus the full text in the presenter notes}
}
@article{MainaAtAl18,
  author = {Solomon Maina and Anders Miltner and Kathleen Fisher
                  and Benjamin C. Pierce and David Walker and
                  Steve Zdancewic},
  title = {Synthesizing Quotient Lenses},
  journal = {Proceedings of the ACM on Programming Languages
                  (PACMPL ICFP)},
  month = sep,
  year = 2018,
  plclub = {Yes},
  bcp = {Yes},
  keys = {misc},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/icfp18-synthesizing-quotient-lenses.pdf},
  keys = {harmony}
}
@inproceedings{CPP-2019,
  author = {Nicolas Koh and
                  Yao Li and
                  Yishuai Li and
                  Li-yao Xia and
                  Lennart Beringer and
                  Wolf Honore and
                  William Mansky and
                  Benjamin C. Pierce and
                  Steve Zdancewic},
  title = {From {C} to Interaction Trees: {S}pecifying, Verifying,
                  and Testing a Networked Server},
  booktitle = {8th ACM SIGPLAN International Conference on Certified Programs and Proofs},
  month = jan,
  year = 2019,
  plclub = {Yes},
  bcp = {Yes},
  keys = {misc},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/deepweb-cpp-2019.pdf}
}
@article{DBLP:journals/pacmpl/Lampropoulos0P19,
  author = {Leonidas Lampropoulos and
               Michael Hicks and
               Benjamin C. Pierce},
  title = {Coverage guided, property based testing},
  journal = {Proc. {ACM} Program. Lang.},
  volume = {3},
  number = {{OOPSLA}},
  pages = {181:1--181:29},
  year = {2019},
  url = {https://doi.org/10.1145/3360607},
  doi = {10.1145/3360607},
  timestamp = {Thu, 16 Apr 2020 13:51:47 +0200},
  biburl = {https://dblp.org/rec/journals/pacmpl/Lampropoulos0P19.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  bcp = {Yes},
  plclub = {Yes},
  keys = {verification}
}
@article{DBLP:journals/pacmpl/MiltnerMFPWZ19,
  author = {Anders Miltner and
               Solomon Maina and
               Kathleen Fisher and
               Benjamin C. Pierce and
               David Walker and
               Steve Zdancewic},
  title = {Synthesizing symmetric lenses},
  journal = {Proc. {ACM} Program. Lang.},
  volume = {3},
  number = {{ICFP}},
  pages = {95:1--95:28},
  year = {2019},
  url = {https://doi.org/10.1145/3341699},
  doi = {10.1145/3341699},
  timestamp = {Thu, 16 Apr 2020 13:51:45 +0200},
  biburl = {https://dblp.org/rec/journals/pacmpl/MiltnerMFPWZ19.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  bcp = {Yes},
  plclub = {Yes},
  keys = {harmony}
}
@article{DBLP:journals/pacmpl/ZhangRHP019,
  author = {Hengchu Zhang and Edo Roth and Andreas Haeberlen and
                  Benjamin C. Pierce and Aaron Roth},
  title = {Fuzzi: a three-level logic for differential privacy},
  journal = {Proc. {ACM} Program. Lang.},
  volume = 3,
  number = {{ICFP}},
  pages = {93:1--93:28},
  year = 2019,
  url = {https://doi.org/10.1145/3341697},
  doi = {10.1145/3341697},
  timestamp = {Thu, 16 Apr 2020 13:51:45 +0200},
  biburl = {https://dblp.org/rec/journals/pacmpl/ZhangRHP019.bib},
  bibsource = {dblp computer science bibliography,
                  https://dblp.org},
  bcp = {Yes},
  plclub = {Yes},
  keys = {security}
}
@misc{Pierce:POPLMarkRetrospective2020,
  author = {Benjamin C. Pierce},
  title = {POPLmark 15 Year Retrospective Panel at {\em
                  Certified Programs and Proofs}},
  year = 2020,
  url = {https://www.youtube.com/watch?v=2M2ZWNzpzkE},
  bcp = {Yes},
  plclub = {Yes},
  keys = {verification},
  note = {Written up in
                  \URL{https://blog.sigplan.org/2020/01/29/mechanized-proofs-for-pl-past-present-and-future/}}
}
@article{DUPLICATE:Zhang:OOPSLA2020,
  author = {Hengchu Zhang and
               Edo Roth and
               Andreas Haeberlen and
               Benjamin C. Pierce and
               Aaron Roth},
  title = {Testing Differential Privacy with Dual Interpreters},
  journal = {Proc. {ACM} Program. Lang.},
  number = {{OOPSLA}},
  year = {2020},
  bcp = {Yes},
  plclub = {Yes},
  keys = {security}
}
@article{Lehsani2022:newer,
  title = {Modular Mechanized Verification of Transactional Predication},
  author = {Mohsen Lesani and {Li-Yao} Xia and Anders Kaseorg and
          Christian J. Bell and
          Adam Chlipala and Benjamin C. Pierce and Steve Zdancewic},
  journal = {Proc. {ACM} Program. Lang.},
  volume = {6},
  number = {{OOPSLA1}},
  month = apr,
  year = {2022},
  bcp = {Yes},
  plclub = {Yes},
  keys = {verification},
  note = {OOPSLA 2022},
  pdef = {http://www.cis.upenn.edu/~bcpierce/papers/oopsla22main-p66-p-3e39fed5de-56232-final.pdf}
}
@article{10.1145/3527324,
  author = {Lesani, Mohsen and Xia, Li-Yao and Kaseorg, Anders and Bell, Christian J. and Chlipala, Adam and Pierce, Benjamin C. and Zdancewic, Steve},
  title = {C4: Verified Transactional Objects},
  year = {2022},
  issue_date = {April 2022},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {6},
  number = {OOPSLA1},
  url = {https://doi.org/10.1145/3527324},
  doi = {10.1145/3527324},
  abstract = {Transactional objects combine the performance of classical concurrent objects with the high-level programmability of transactional memory. However, verifying the correctness of transactional objects is tricky, requiring reasoning simultaneously about classical concurrent objects, which guarantee the atomicity of individual methods—the property known as linearizability—and about software-transactional-memory libraries, which guarantee the atomicity of user-defined sequences of method calls—or serializability. We present a formal-verification framework called C4, built up from the familiar notion of linearizability and its compositional properties, that allows proof of both kinds of libraries, along with composition of theorems from both styles to prove correctness of applications or further libraries. We apply the framework in a significant case study, verifying a transactional set object built out of both classical and transactional components following the technique of transactional predication; the proof is modular, reasoning separately about the transactional and nontransactional parts of the implementation. Central to our approach is the use of syntactic transformers on interaction trees—i.e., transactional libraries that transform client code to enforce particular synchronization disciplines. Our framework and case studies are mechanized in Coq.},
  journal = {Proc. ACM Program. Lang.},
  month = {apr},
  articleno = {80},
  numpages = {31},
  keywords = {objects, serializability, concurrency, verification, linearizability},
  bcp = {Yes},
  plclub = {Yes},
  keys = {verification}
}
@article{DBLP:journals/pacmpl/XiaZHHMPZ20,
  author = {Li{-}yao Xia and
               Yannick Zakowski and
               Paul He and
               Chung{-}Kil Hur and
               Gregory Malecha and
               Benjamin C. Pierce and
               Steve Zdancewic},
  title = {Interaction trees: representing recursive and impure programs in Coq},
  journal = {Proc. {ACM} Program. Lang.},
  volume = {4},
  number = {{POPL}},
  pages = {51:1--51:32},
  year = {2020},
  url = {https://doi.org/10.1145/3371119},
  doi = {10.1145/3371119},
  timestamp = {Thu, 16 Apr 2020 13:51:44 +0200},
  biburl = {https://dblp.org/rec/journals/pacmpl/XiaZHHMPZ20.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  note = {Distinguished paper award},
  bcp = {Yes},
  plclub = {Yes},
  keys = {verification}
}
@article{DBLP:journals/cacm/PierceHLP20,
  author = {Benjamin C. Pierce and
               Michael Hicks and
               Crista Lopes and
               Jens Palsberg},
  title = {Conferences in an era of expensive carbon},
  journal = {Commun. {ACM}},
  volume = {63},
  number = {3},
  pages = {35--37},
  year = {2020},
  url = {https://doi.org/10.1145/3380445},
  doi = {10.1145/3380445},
  timestamp = {Tue, 10 Mar 2020 09:08:18 +0100},
  biburl = {https://dblp.org/rec/journals/cacm/PierceHLP20.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  bcp = {Yes},
  plclub = {Yes},
  keys = {misc,climate}
}
@misc{VirtualConferencesPTP,
  author = {{ACM Presidential Task Force on What Conferences
                  Can Do to Replace Face to Face Meetings
                  (co-chairs, Crista Lopes and Jeanna Matthews;
                  executive editor, Benjamin C. Pierce)}},
  title = {Virtual Conferences: {A} Guide to Best Practices},
  year = 2020,
  month = may,
  note = {\URL{https://www.acm.org/virtual-conferences}},
  bcp = {Yes},
  plclub = {Yes},
  keys = {misc,climate}
}
@misc{VirtualConferencesNorthstar2020,
  author = {Crista Videira Lopes and Jeanna Matthews and Benjamin Pierce},
  title = {Best Practices for Planning Virtual Conferences},
  year = 2020,
  month = may,
  note = {Northstar Meetings Group blog, \URL{https://www.northstarmeetingsgroup.com/Planning-Tips-and-Trends/Event-Planning/Event-Technology/Navigating-New-World-Virtual-Digital-Conferences-in-COVID19-ACM}},
  bcp = {Yes},
  plclub = {Yes},
  keys = {misc,climate}
}
@article{DBLP:journals/corr/abs-2104-01239,
  author = {Stephanie Weirich and
               Benjamin C. Pierce},
  title = {{ICFP} 2020 Post-Conference Report},
  journal = {CoRR},
  volume = {abs/2104.01239},
  year = {2021},
  url = {https://arxiv.org/abs/2104.01239},
  archiveprefix = {arXiv},
  eprint = {2104.01239},
  timestamp = {Mon, 12 Apr 2021 16:14:56 +0200},
  biburl = {https://dblp.org/rec/journals/corr/abs-2104-01239.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  bcp = {Yes},
  plclub = {Yes},
  keys = {misc}
}
@inproceedings{Li2021:MBToNA,
  author = {Yishuai Li and
                  Benjamin C. Pierce and
                  Steve Zdancewic},
  editor = {Cristian Cadar and
                  Xiangyu Zhang},
  title = {Model-based testing of networked applications},
  booktitle = {{ISSTA} '21: 30th {ACM} {SIGSOFT} International Symposium on Software
                  Testing and Analysis, Virtual Event, Denmark, July 11-17, 2021},
  pages = {529--539},
  publisher = {{ACM}},
  year = {2021},
  url = {https://doi.org/10.1145/3460319.3464798},
  doi = {10.1145/3460319.3464798},
  timestamp = {Sat, 08 Jan 2022 02:24:32 +0100},
  biburl = {https://dblp.org/rec/conf/issta/LiPZ21.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  bcp = {Yes},
  plclub = {Yes},
  keys = {verification}
}
@inproceedings{DBLP:conf/esop/GoldsteinHLP21,
  author = {Harrison Goldstein and
                  John Hughes and
                  Leonidas Lampropoulos and
                  Benjamin C. Pierce},
  editor = {Nobuko Yoshida},
  title = {Do Judge a Test by its Cover: Combining Combinatorial
                  and Property-Based Testing},
  booktitle = {Programming Languages and Systems, 30th European Symposium on Programming,
                  {ESOP} 2021, Held as Part of the European Joint Conferences on Theory
                  and Practice of Software, {ETAPS} 2021, Luxembourg City, Luxembourg,
                  March 27 - April 1, 2021, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {12648},
  pages = {264--291},
  publisher = {Springer},
  year = {2021},
  url = {https://doi.org/10.1007/978-3-030-72019-3\_10},
  doi = {10.1007/978-3-030-72019-3\_10},
  timestamp = {Wed, 07 Apr 2021 16:01:48 +0200},
  biburl = {https://dblp.org/rec/conf/esop/GoldsteinHLP21.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  bcp = {Yes},
  plclub = {Yes},
  keys = {misc,verification}
}
@inproceedings{Anderson2021stack,
  author = {Sean Noble Anderson and
                  Leonidas Lampropoulos and
                  Roberto Blanco and
                  Benjamin C. Pierce and
                  Andrew Tolmach},
  title = {Security Properties for Stack Safety},
  year = {2021},
  booktitle = {Workshop on Foundations of Computer Security (FCS)},
  bcp = {Yes},
  plclub = {Yes},
  keys = {misc,verification}
}
@article{Anderson2021stack:old2,
  author = {Sean Noble Anderson and
                  Leonidas Lampropoulos and
                  Roberto Blanco and
                  Benjamin C. Pierce and
                  Andrew Tolmach},
  title = {Security Properties for Stack Safety},
  journal = {CoRR},
  volume = {abs/2105.00417},
  year = {2021},
  url = {https://arxiv.org/abs/2105.00417},
  eprinttype = {arXiv},
  eprint = {2105.00417},
  timestamp = {Wed, 12 May 2021 15:54:31 +0200},
  biburl = {https://dblp.org/rec/journals/corr/abs-2105-00417.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  bcp = {Yes},
  plclub = {Yes},
  keys = {misc,verification}
}
@article{DBLP:journals/pacmpl/ZhangRHP020,
  author = {Hengchu Zhang and
               Edo Roth and
               Andreas Haeberlen and
               Benjamin C. Pierce and
               Aaron Roth},
  title = {Testing Differential Privacy with Dual Interpreters},
  journal = {Proc. {ACM} Program. Lang.},
  volume = {4},
  number = {{OOPSLA}},
  pages = {165:1--165:26},
  year = {2020},
  url = {https://doi.org/10.1145/3428233},
  doi = {10.1145/3428233},
  timestamp = {Wed, 17 Feb 2021 08:54:06 +0100},
  biburl = {https://dblp.org/rec/journals/pacmpl/ZhangRHP020.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  note = {Selected for a Distinguished Artifact Award},
  bcp = {Yes},
  plclub = {Yes},
  keys = {privacy}
}
@inproceedings{Anderson2023stack,
  title = {Stack Safety as a Security Property},
  author = {Anderson, Sean Noble and Lampropoulos, Leonidas and
    Blanco, Roberto and Pierce, Benjamin C. and Tolmach, Andrew},
  year = {2023},
  booktitle = {IEEE Symposium on Computer Security Foundations (CSF)},
  shortbooktitle = {CSF},
  publisher = {IEEE Computer Society Press},
  plclub = {Yes},
  bcp = {Yes},
  keys = {security}
}
@inproceedings{DBLP:conf/chi/BietzGIMMPRW22,
  author = {Matthew J. Bietz and
               Nitesh Goyal and
               Nicole Immorlica and
               Blair MacIntyre and
               Andr{\'{e}}s Monroy{-}Hern{\'{a}}ndez and
               Benjamin C. Pierce and
               Sean Rintel and
               Donghee Yvette Wohn},
  editor = {Simone D. J. Barbosa and
               Cliff Lampe and
               Caroline Appert and
               David A. Shamma},
  title = {Social Presence in Virtual Event Spaces},
  booktitle = {{CHI} '22: {CHI} Conference on Human Factors in Computing Systems,
               New Orleans, LA, USA, 29 April 2022 - 5 May 2022, Extended Abstracts},
  pages = {106:1--106:5},
  publisher = {{ACM}},
  year = {2022},
  url = {https://doi.org/10.1145/3491101.3503713},
  doi = {10.1145/3491101.3503713},
  timestamp = {Wed, 04 May 2022 13:02:17 +0200},
  biburl = {https://dblp.org/rec/conf/chi/BietzGIMMPRW22.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  bcp = {Yes},
  plclub = {Yes},
  keys = {climate}
}
@article{DBLP:journals/corr/abs-2203-00652,
  author = {Harrison Goldstein and
                  Benjamin C. Pierce},
  title = {Parsing Randomness: Unifying and Differentiating Parsers and Random
                  Generators},
  journal = {CoRR},
  volume = {abs/2203.00652},
  year = {2022},
  url = {https://doi.org/10.48550/arXiv.2203.00652},
  doi = {10.48550/arXiv.2203.00652},
  eprinttype = {arXiv},
  eprint = {2203.00652},
  timestamp = {Wed, 16 Mar 2022 16:39:52 +0100},
  biburl = {https://dblp.org/rec/journals/corr/abs-2203-00652.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  bcp = {Yes},
  plclub = {Yes},
  keys = {verification}
}
@inproceedings{DBLP:conf/itp/ZhangHK0LXBMPZ21,
  author = {Hengchu Zhang and
                  Wolf Honor{\'{e}} and
                  Nicolas Koh and
                  Yao Li and
                  Yishuai Li and
                  Li{-}yao Xia and
                  Lennart Beringer and
                  William Mansky and
                  Benjamin C. Pierce and
                  Steve Zdancewic},
  editor = {Liron Cohen and
                  Cezary Kaliszyk},
  title = {Verifying an {HTTP} Key-Value Server with Interaction Trees and {VST}},
  booktitle = {12th International Conference on Interactive Theorem Proving, {ITP}
                  2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)},
  series = {LIPIcs},
  volume = {193},
  pages = {32:1--32:19},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year = {2021},
  url = {https://doi.org/10.4230/LIPIcs.ITP.2021.32},
  doi = {10.4230/LIPIcs.ITP.2021.32},
  timestamp = {Sat, 09 Apr 2022 12:45:06 +0200},
  biburl = {https://dblp.org/rec/conf/itp/ZhangHK0LXBMPZ21.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  bcp = {Yes},
  plclub = {Yes},
  keys = {verification}
}
@article{DreyerPierce2022,
  author = {Derek Dreyer and
                  Benjamin C. Pierce},
  title = {On being a {PhD} student of {R}obert {H}arper},
  journal = {Journal of Functional Programming},
  volume = {32.32},
  year = {2022},
  bcp = {Yes},
  plclub = {Yes},
  keys = {misc}
}
@misc{Holey2022,
  author = {Joseph Cutler and Harrison Goldstein and Koen Claessen
                  and John Hughes and Benjamin C. Pierce },
  title = {Functional Pearl: Holey Generators!},
  year = 2022,
  month = may,
  note = {Draft},
  bcp = {Yes},
  plclub = {Yes},
  keys = {verification}
}
@misc{Frohlich2023old,
  author = {Harrison Goldstein and Samantha Frohlich and
                  Benjamin C. Pierce and Meng Wang},
  title = {Reflecting on Random Generation},
  year = 2023,
  month = feb,
  note = {Under submission},
  bcp = {Yes},
  plclub = {Yes},
  keys = {verification}
}
@article{goldstein2023reflecting,
  title = {Reflecting on Random Generation},
  author = {Goldstein, Harrison and Frohlich, Samantha and
                  Wang, Meng and Pierce, Benjamin C},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {7},
  number = {ICFP},
  pages = {322--355},
  year = {2023},
  bcp = {Yes},
  plclub = {Yes},
  keys = {verification},
  publisher = {ACM New York, NY, USA}
}
@misc{GoldsteinChoices2022,
  author = {Harrison Goldstein and
                  Benjamin C. Pierce},
  title = {Making Better Choices: {G}uiding Random Generators with Derivatives},
  year = 2022,
  note = {Draft},
  bcp = {Yes},
  plclub = {Yes},
  keys = {verification}
}
@misc{Pierce:Yow22,
  author = {Benjamin C. Pierce},
  title = {({W}hen) Will Property-Based Testing Rule The World?},
  month = may,
  year = 2022,
  note = {Keynote at {\it Yow! Lambda Jam} Conference},
  plclub = {Yes},
  bcp = {Yes},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/Yow2022-Pierce.pdf},
  keys = {verification}
}
@misc{Pierce:2.8:2022,
  author = {Benjamin C. Pierce},
  title = {Understanding Property-Based Testing by Talking to People},
  month = may,
  year = 2022,
  note = {Short talk at {\it Working Group 2.8}},
  plclub = {Yes},
  bcp = {Yes},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/Pierce-WG2.8-2022.pdf},
  keys = {verification}
}
@article{10.1145/3527324-duplicate,
  author = {Lesani, Mohsen and Xia, Li-yao and Kaseorg, Anders and Bell, Christian J. and Chlipala, Adam and Pierce, Benjamin C. and Zdancewic, Steve},
  title = {C4: Verified Transactional Objects},
  year = {2022},
  issue_date = {April 2022},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {6},
  number = {OOPSLA1},
  url = {https://doi.org/10.1145/3527324},
  doi = {10.1145/3527324},
  abstract = {Transactional objects combine the performance of classical concurrent objects with the high-level programmability of transactional memory. However, verifying the correctness of transactional objects is tricky, requiring reasoning simultaneously about classical concurrent objects, which guarantee the atomicity of individual methods—the property known as linearizability—and about software-transactional-memory libraries, which guarantee the atomicity of user-defined sequences of method calls—or serializability. We present a formal-verification framework called C4, built up from the familiar notion of linearizability and its compositional properties, that allows proof of both kinds of libraries, along with composition of theorems from both styles to prove correctness of applications or further libraries. We apply the framework in a significant case study, verifying a transactional set object built out of both classical and transactional components following the technique of transactional predication; the proof is modular, reasoning separately about the transactional and nontransactional parts of the implementation. Central to our approach is the use of syntactic transformers on interaction trees—i.e., transactional libraries that transform client code to enforce particular synchronization disciplines. Our framework and case studies are mechanized in Coq.},
  journal = {Proc. ACM Program. Lang.},
  month = {apr},
  articleno = {80},
  numpages = {31},
  keywords = {concurrency, serializability, linearizability, verification, objects},
  plclub = {Yes},
  bcp = {Yes},
  keys = {verification}
}
@article{GoldsteinOOPSLA2022,
  author = {Goldstein, Harrison and Pierce, Benjamin C.},
  title = {Parsing Randomness},
  year = {2022},
  issue_date = {October 2022},
  number = {OOPSLA},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  journal = {Proc. ACM Program. Lang.},
  plclub = {Yes},
  bcp = {Yes},
  paper = {http://www.cis.upenn.edu/~bcpierce/papers/oopsla22.pdf},
  keys = {verification}
}
@inproceedings{10.1145/3491101.3503713,
  author = {J. Bietz, Matthew and Goyal, Nitesh and Immorlica, Nicole and MacIntyre, Blair and Monroy-Hern\'{a}ndez, Andr\'{e}s and C. Pierce, Benjamin and Rintel, Sean and Wohn, Donghee Yvette},
  title = {Social Presence in Virtual Event Spaces},
  year = {2022},
  isbn = {9781450391566},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  url = {https://doi.org/10.1145/3491101.3503713},
  doi = {10.1145/3491101.3503713},
  abstract = {It is generally acknowledged that the virtual event platforms of today do not perform satisfactorily at what is arguably their most important function: providing attendees with a sense of social presence. Social presence is the “sense of being with another” and can include ways of knowing who is in the virtual space, how others are reacting to what is happening in the space, an awareness of others’ activities and availability, and an idea of how to connect with them. Issues around presence and awareness have been perennial topics in the CHI and CSCW communities for decades. Nevertheless, the time feels ripe for a new effort with a special focus on larger-scale virtual events, given the accelerated pace of change in the socio-technological landscape and the tremendous potential impact that new insights could now have. The goal of this workshop is to bring together researchers and developers from academia and industry with a shared interest in improving the experience of virtual events to exchange insights and hopefully energize an ongoing community effort in this area.},
  booktitle = {CHI Conference on Human Factors in Computing Systems Extended Abstracts},
  articleno = {106},
  numpages = {5},
  keywords = {Virtual conventions, Virtual conferences, Virtual meetings, Awareness, Social presence},
  location = {New Orleans, LA, USA},
  series = {CHI EA '22},
  plclub = {Yes},
  bcp = {Yes},
  keys = {climate,misc}
}
@misc{Pierce:LambdaTA2022,
  author = {Benjamin C. Pierce},
  title = {Software Foundations, 15 years on},
  day = 20,
  month = jul,
  year = 2022,
  note = {Talk at Newton Institute workshop on Formal Education},
  plclub = {Yes},
  bcp = {Yes},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/LambdaTA-Newton.pdf},
  keys = {verification}
}
@misc{Pierce:ImaginingTheReader2023,
  author = {Benjamin C. Pierce},
  title = {Imagining the Reader},
  day = 20,
  month = jul,
  year = 2022,
  note = {Talk at Programming Languages Mentoring Workshop (PLMW)},
  plclub = {Yes},
  bcp = {Yes},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/PLMW2023-ImaginingTheReader.pdf},
  keys = {misc}
}
@inproceedings{Shi2023,
  author = {Jessica Shi and Benjamin Pierce and Andrew Head},
  title = {Towards a Science of Interactive Proof Reading},
  year = {2023},
  booktitle = {13th annual workshop on the intersection of HCI and PL (PLATEAU)},
  bcp = {Yes},
  plclub = {Yes},
  keys = {misc,verification}
}
@misc{cutler2023stream,
  title = {Stream Types},
  author = {Joseph W. Cutler and Christopher Watson and
              Phillip Hilliard and Harrison Goldstein and
              Caleb Stanford and Benjamin C. Pierce},
  year = {2023},
  eprint = {2307.09553},
  archiveprefix = {arXiv},
  primaryclass = {cs.PL},
  url = {https://arxiv.org/abs/2307.09553},
  bcp = {Yes},
  plclub = {Yes}
}
@article{shi2023etna,
  title = {Etna: An Evaluation Platform for Property-Based Testing
                  (Experience Report)},
  author = {Shi, Jessica and Keles, Alperen and Goldstein, Harrison
                  and Pierce, Benjamin C and Lampropoulos, Leonidas},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {7},
  number = {ICFP},
  pages = {878--894},
  year = {2023},
  bcp = {Yes},
  plclub = {Yes},
  paper = {http://www.cis.upenn.edu/~bcpierce/papers/etna2023.pdf},
  publisher = {ACM New York, NY, USA}
}
@misc{Pierce:Subtyping2023,
  author = {Benjamin C. Pierce},
  title = {What Does Subtyping Mean?},
  day = 4,
  month = aug,
  year = 2023,
  note = {Talk at Programming Languages Mentoring Workshop (PLMW)},
  plclub = {Yes},
  bcp = {Yes},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/2023-PLMW-Subtyping.pdf},
  keys = {types}
}
@inproceedings{Goldstein2024ICSE,
  title = {Property-Based Testing in Practice},
  author = {Harrison Goldstein and Joseph W. Cutler and
                  Daniel Dickstein and Benjamin C. Pierce and Andrew Head},
  year = {2024},
  booktitle = {International Conference on Software Engineering (ICSE)},
  url = {https://harrisongoldste.in/papers/icse24-pbt-in-practice.pdf},
  bcp = {Yes},
  plclub = {Yes}
}
@inproceedings{goldstein_property-based_2024,
  title = {Property-{Based} {Testing} in {Practice}},
  booktitle = {International {Conference} on {Software} {Engineering} ({ICSE})},
  author = {Goldstein, Harrison and Cutler, Joseph W and Dickstein, Daniel and Pierce, Benjamin C and Head, Andrew},
  year = {2024},
  url = {http://www.cis.upenn.edu/~bcpierce/papers/icse24-pbt-in-practice},
  bcp = {Yes},
  plclub = {Yes},
  keys = {testing}
}
@misc{Pierce:TFP24,
  author = {Benjamin C. Pierce},
  title = {delta: Ordered Types for Stream Processing},
  day = 10,
  month = jan,
  year = 2024,
  note = {Talk at Trends in Functional Programming (TFP)},
  plclub = {Yes},
  bcp = {Yes},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/2024-TFP-talk.pdf},
  keys = {types}
}
@misc{Pierce:POPL24ClimateTalk,
  author = {Benjamin C. Pierce},
  title = {},
  day = 17,
  month = jan,
  year = 2024,
  note = {Short talk at POPL reception},
  plclub = {Yes},
  bcp = {Yes},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/2024-POPL-reception-talk.pdf},
  keys = {climate}
}
@unpublished{HosoyaPierceTurner98,
  author = {Haruo Hosoya and Benjamin C. Pierce and David N. Turner},
  title = {Datatypes and Subtyping},
  note = {Manuscript},
  plclub = {Yes},
  bcp = {Yes},
  keys = {subtyping},
  year = 1998,
  ps = {http://www.cis.upenn.edu/~bcpierce/ds.ps}
}
@phdthesis{LiYishuaiThesis,
  author = {Yishuai Li},
  title = {Testing By Dualization},
  year = {2022},
  school = {University of Pennsylvania},
  url = {https://repository.upenn.edu/edissertations/5376/},
  bcp = {Yes},
  plclub = {Yes},
  keys = {verification}
}
@phdthesis{XiaLiYao,
  author = {Li-Yao Xia},
  title = {Executable Semantics with Interaction Trees},
  year = {2022},
  school = {University of Pennsylvania},
  url = {https://repository.upenn.edu/edissertations/5348/},
  bcp = {Yes},
  plclub = {Yes},
  keys = {verification}
}