bcp.bib

@preamble{{\newcommand{\SortNoop}[1]{}}}

@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 = {2023},
  publisher = {Electronic textbook},
  plclub = {Yes},
  bcp = {Yes},
  keys = {verification,books},
  note = {Version 6.6.  \URL{http://www.cis.upenn.edu/~bcpierce/sf}},
  ebook = {http://www.cis.upenn.edu/~bcpierce/sf}
}

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

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

@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:old,
  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},
  number = {ICFP},
  year = {2024},
  bcp = {Yes},
  plclub = {Yes},
  keys = {types},
  note = {To appear}
}

@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{cutler2024stream,
  title = {Stream Types},
  author = {Joseph W. Cutler and Christopher Watson and
                  Phillip Hilliard and Harrison Goldstein and
                  Caleb Stanford and Benjamin C. Pierce},
  journal = {Proceedings of the ACM on Programming Languages},
  number = {PLDI},
  year = {2024},
  url = {https://arxiv.org/abs/2307.09553},
  bcp = {Yes},
  plclub = {Yes},
  note = {To appearJ. W. Cutler, C. Watson, P. Hilliard, H. Goldstein, C. Stanford, and B. C. Pierce, “Stream types,” Proceed- ings of the ACM on Programming Languages, no. PLDI, 2024. To appear.}
}

@misc{cutler2023stream:old,
  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{goldstein_problems_2022_HATRA,
  title = {Some {Problems} with {Properties}},
  volume = {1},
  url = {https://harrisongoldste.in/papers/hatra2022.pdf},
  booktitle = {Workshop on Human Aspects of Types and Reasoning Assistants (HATRA)},
  language = {en},
  author = {Goldstein, Harrison and Cutler, Joseph W. and Stein,
                  Adam and Pierce, Benjamin C. and Head, Andrew},
  month = dec,
  year = {2022},
  file = {Goldstein et al. - Some Problems with Properties.pdf:/Users/harrison/Zotero/storage/QVA4RMQP/Goldstein et al. - Some Problems with Properties.pdf:application/pdf},
  bcp = {Yes},
  plclub = {Yes},
  keys = {testing}
}

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

@misc{goldstein_tyche_2023,
  address = {San Francisco, CA, USA},
  type = {Demo},
  title = {Tyche: {In} {Situ} {Exploration} of {Random} {Testing} {Effectiveness} ({Demo})},
  copyright = {All rights reserved},
  url = {https://harrisongoldste.in/papers/uist23.pdf},
  author = {Goldstein, Harrison},
  collaborator = {Pierce, Benjamin C and Head, Andrew},
  month = oct,
  year = {2023},
  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}
}

@inproceedings{goldstein_property-based_2024,
  address = {Lisbon, Portugal},
  series = {{ICSE} '24},
  title = {Property-{Based} {Testing} in {Practice}},
  volume = {187},
  copyright = {All rights reserved},
  isbn = {9798400702174},
  url = {https://doi.org/10.1145/3597503.3639581},
  doi = {10.1145/3597503.3639581},
  abstract = {Property-based testing (PBT) is a testing methodology where users write executable formal specifications of software components and an automated harness checks these specifications against many automatically generated inputs. From its roots in the QuickCheck library in Haskell, PBT has made significant inroads in mainstream languages and industrial practice at companies such as Amazon, Volvo, and Stripe. As PBT extends its reach, it is important to understand how developers are using it in practice, where they see its strengths and weaknesses, and what innovations are needed to make it more effective.
We address these questions using data from 30 in-depth interviews with experienced users of PBT at Jane Street, a financial technology company making heavy and sophisticated use of PBT. These interviews provide empirical evidence that PBT's main strengths lie in testing complex code and in increasing confidence beyond what is available through conventional testing methodologies, and, moreover, that most uses fall into a relatively small number of high-leverage idioms. Its main weaknesses, on the other hand, lie in the relative complexity of writing properties and random data generators and in the difficulty of evaluating their effectiveness. From these observations, we identify a number of potentially high-impact areas for future exploration, including performance improvements, differential testing, additional high-leverage testing scenarios, better techniques for generating random input data, test-case reduction, and methods for evaluating the effectiveness of tests.},
  language = {en},
  booktitle = {Proceedings of the {IEEE}/{ACM} 46th {International} {Conference} on {Software} {Engineering}},
  publisher = {Association for Computing Machinery},
  author = {Goldstein, Harrison and Cutler, Joseph W. and Dickstein, Daniel and Pierce, Benjamin C. and Head, Andrew},
  year = {2024},
  pages = {1--13},
  file = {Goldstein - 2023 - Property-Based Testing in Practice Codebook.pdf:/Users/harrison/Zotero/storage/XRH6XD6C/Goldstein - 2023 - Property-Based Testing in Practice Codebook.pdf:application/pdf},
  bcp = {Yes},
  plclub = {Yes},
  keys = {testing}
}

@misc{goldstein_lucid_2024,
  title = {Lucid {Property}-{Based} {Testing}},
  url = {https://harrisongoldste.in/papers/drafts/uist-2024-lucid.pdf},
  abstract = {Software developers increasingly rely on automated methods to assess the
correctness of their code. One such method is property-based testing
(PBT), wherein a test harness generates hundreds or thousands of inputs
and checks the outputs of the program on those inputs using parametric
properties. Though powerful, PBT itself induces a sizable gulf of
evaluation: developers need to put in nontrivial effort to understand
how well the different test inputs exercise the software under test. To
bridge this gulf, we propose lucid property-based testing, an
interaction paradigm to support sensemaking for PBT effectiveness.
Guided by a formative design exploration, we designed and implemented
LUCID, an interface that supports lucid PBT through interactive,
configurable views of test behavior with tight integrations into modern
developer testing workflow. These views help developers explore global
testing behavior and individual example attributes alike. To accelerate
the development of powerful, interactive PBT tools, we define a standard
for PBT test reporting and integrate it with a widely used PBT library.
A self-guided online usability study revealed that LUCID’s views lead to
better assessments of software testing effectiveness.},
  language = {en},
  author = {Goldstein, Harrison and Tao, Jeffrey and Hatfield-Dodds, Zac and Pierce, Benjamin C. and Head, Andrew},
  year = {2024},
  note = {Under submission},
  bcp = {Yes},
  plclub = {Yes},
  keys = {testing}
}

@inproceedings{10.1145/3654777.3676407,
  author = {Goldstein, Harrison and Tao, Jeffrey and Hatfield-Dodds, Zac and Pierce, Benjamin C. and Head, Andrew},
  title = {Tyche: Making Sense of PBT Effectiveness},
  year = {2024},
  isbn = {9798400706288},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  url = {https://doi.org/10.1145/3654777.3676407},
  doi = {10.1145/3654777.3676407},
  abstract = {Software developers increasingly rely on automated methods to assess the correctness of their code. One such method is property-based testing (PBT), wherein a test harness generates hundreds or thousands of inputs and checks the outputs of the program on those inputs using parametric properties. Though powerful, PBT induces a sizable gulf of evaluation: developers need to put in nontrivial effort to understand how well the different test inputs exercise the software under test. To bridge this gulf, we propose Tyche, a user interface that supports sensemaking around the effectiveness of property-based tests. Guided by a formative design exploration, our design of Tyche supports developers with interactive, configurable views of test behavior with tight integrations into modern developer testing workflow. These views help developers explore global testing behavior and individual test inputs alike. To accelerate the development of powerful, interactive PBT tools, we define a standard for PBT test reporting and integrate it with a widely used PBT library. A self-guided online usability study revealed that Tyche’s visualizations help developers to more accurately assess software testing effectiveness.},
  booktitle = {Proceedings of the 37th Annual ACM Symposium on User Interface Software and Technology},
  articleno = {10},
  numpages = {16},
  keywords = {Randomized testing, multiple program executions, property-based testing (PBT), visual feedback},
  location = {Pittsburgh, PA, USA},
  series = {UIST '24},
  bcp = {Yes},
  plclub = {Yes},
  keys = {testing}
}

@misc{INT-talk-2024,
  author = {Hughes, John and Bannerjee, Rini and Pierce, Benjamin C.},
  title = {Adventures in Specification-Based Testing},
  note = {Invited talk at Isaac Newton Institute
                  Workshop on Big Specification:
                  Specification, Proof, and Testing at Scale},
  month = oct,
  slides = {http://www.cis.upenn.edu/~bcpierc/papers/Pierce-2024-INI-talk.pdf},
  year = 2024,
  bcp = {Yes},
  plclub = {Yes},
  keys = {testing}
}

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