bcp.bib

@preamble{{\newcommand{\SortNoop}[1]{}}}
@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}
}
@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{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}
}
@unpublished{InCertProposal06,
  title = {Manifest Security for Distributed Information},
  author = {Karl Crary and  Robert Harper and Frank Pfenning and
                  Benjamin C. Pierce and Stephanie Weirich and 
                  Stephan Zdancewic},
  year = 2006,
  month = mar,
  keys = {security},
  note = {White paper},
  pdf = {http://www.cis.upenn.edu/~bcpierce/papers/incertproposal06.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}
}
@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{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{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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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: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}
}
@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}
}