bcp.bib

@preamble{{\newcommand{\SortNoop}[1]{}}}
@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},
  keys = {verification},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/chalmers-deepspec-2015.pdf}
}
@book{Pierce:SF,
  author = {Benjamin C. Pierce and Arthur Azevedo de Amorim 
                  and Chris Casinghino and Marco Gaboardi and
                  Michael Greenberg and C\v{a}t\v{a}lin Hri\c{t}cu 
                  and Vilhelm Sj\"{o}berg and Brent Yorgey},
  title = {Software Foundations},
  year = {2017},
  publisher = {Electronic textbook},
  plclub = {Yes},
  bcp = {Yes},
  keys = {poplmark,books},
  note = {Version 5.0.  \URL{http://www.cis.upenn.edu/~bcpierce/sf}},
  ebook = {http://www.cis.upenn.edu/~bcpierce/sf},
  japanese = {http://proofcafe.org/sf}
}
@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}
}
@misc{Pierce:SPLASHTalk2016,
  author = {Benjamin C. Pierce},
  title = {The Science of Deep Specification},
  month = nov,
  year = 2016,
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/deepspec-splash2016.pdf},
  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}
}
@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}
}
@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}
}
@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)}
}
@inproceedings{WinogradCort2017,
  author = {Daniel Winograd-Cord and Andreas Haeberlen and
                  Aaron Roth and Benjamin C. Pierce},
  title = {A Framework for Adaptive Differential Privacy},
  booktitle = {{ACM} {SIGPLAN} {I}nternational {C}onference on
                  {F}unctional {P}rogramming ({ICFP})},
  month = sep,
  year = 2017,
  keys = {privacy},
  plclub = {Yes},
  bcp = {Yes}
}
@inproceedings{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 = {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{beginners-luck-old,
  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},
  url = {https://arxiv.org/abs/1607.05443},
  year = {2016},
  month = jul,
  howpublished = {Draft, arXiv:1607.05443},
  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{AzevedoDeAmorim17,
  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},
  howpublished = {arXiv:1705.07354},
  url = {https://arxiv.org/abs/1705.07354},
  year = {2017},
  month = may,
  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}
}
@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: the 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 = {Proceedings of the ACM on Programming Languages (PACMPL)},
  month = jan,
  year = 2018,
  plclub = {Yes},
  bcp = {Yes}
}
@article{Lampropoulos&18,
  author = {Leonidas Lampropoulos and
                  Zoe Paraskevopoulou and
                  Benjamin C. Pierce },
  title = {Generating Good Generators for Inductive Relations},
  journal = {Proceedings of the ACM on Programming Languages (PACMPL)},
  month = jan,
  year = 2018,
  plclub = {Yes},
  bcp = {Yes}
}
@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.0)},
  month = nov,
  year = 2017,
  short = {http://www.cis.upenn.edu/~bcpierce/papers/sigplan-climate-report.pdf},
  plclub = {Yes},
  bcp = {Yes},
  keys = {misc}
}