bcp.bib

@preamble{{\newcommand{\SortNoop}[1]{}}}
@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: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}
}
@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{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}
}
@misc{Aydemir07a:old,
  author = {Brian Aydemir and Arthur Chargu{{\'e}}raud and Benjamin C. Pierce
                  and Randy Pollack and Stephanie Weirich},
  title = {Engineering Formal Metatheory},
  year = {2007},
  month = jul,
  keys = {verification},
  note = {Submitted for publication},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/binders.pdf}
}
@misc{Pierce08LambdaTA,
  author = {Benjamin C. Pierce},
  title = {Using a Proof Assistant to Teach Programming Language Foundations, or,
                  {L}ambda, the Ultimate {TA}},
  year = {2008},
  month = apr,
  bcp = {Yes},
  keys = {verification},
  plclub = {Yes},
  note = {White paper},
  short = {http://www.cis.upenn.edu/~bcpierce/papers/plcurriculum.pdf}
}
@book{Pierce:SFold,
  author = {Benjamin C. Pierce and Arthur {Azevedo de Amorim}
                  and Chris Casinghino and Marco Gaboardi and
                  Michael Greenberg and C\v{a}t\v{a}lin Hri\c{t}cu
                  and Vilhelm Sj\"{o}berg and Brent Yorgey},
  title = {Software Foundations},
  year = {2017},
  publisher = {Electronic textbook},
  plclub = {Yes},
  bcp = {Yes},
  keys = {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}
}
@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.}
}
@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{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{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)}
}
@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{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},
  keys = {verification}
}
@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{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}
}
@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}
}
@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{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}
}
@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/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}
}
@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}
}
@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}
}
@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}
}
@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}
}