bcp.bib

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

@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,
  title = {Reflecting on Random Generation},
  author = {Goldstein, Harrison and Frohlich, Samantha and
                  Wang, Meng and Pierce, Benjamin C},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {7},
  number = {ICFP},
  pages = {322--355},
  year = {2023},
  bcp = {Yes},
  plclub = {Yes},
  keys = {verification},
  publisher = {ACM New York, NY, USA}
}

@misc{GoldsteinChoices2022,
  author = {Harrison Goldstein and
                  Benjamin C. Pierce},
  title = {Making Better Choices: {G}uiding Random Generators with Derivatives},
  year = 2022,
  note = {Draft},
  bcp = {Yes},
  plclub = {Yes},
  keys = {verification}
}

@misc{Pierce:Yow22,
  author = {Benjamin C. Pierce},
  title = {({W}hen) Will Property-Based Testing Rule The World?},
  month = may,
  year = 2022,
  note = {Keynote at {\it Yow! Lambda Jam} Conference},
  plclub = {Yes},
  bcp = {Yes},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/Yow2022-Pierce.pdf},
  keys = {verification}
}

@misc{Pierce:2.8:2022,
  author = {Benjamin C. Pierce},
  title = {Understanding Property-Based Testing by Talking to People},
  month = may,
  year = 2022,
  note = {Short talk at {\it Working Group 2.8}},
  plclub = {Yes},
  bcp = {Yes},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/Pierce-WG2.8-2022.pdf},
  keys = {verification}
}

@article{10.1145/3527324-duplicate,
  author = {Lesani, Mohsen and Xia, Li-yao and Kaseorg, Anders and Bell, Christian J. and Chlipala, Adam and Pierce, Benjamin C. and Zdancewic, Steve},
  title = {C4: Verified Transactional Objects},
  year = {2022},
  issue_date = {April 2022},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {6},
  number = {OOPSLA1},
  url = {https://doi.org/10.1145/3527324},
  doi = {10.1145/3527324},
  abstract = {Transactional objects combine the performance of classical concurrent objects with the high-level programmability of transactional memory. However, verifying the correctness of transactional objects is tricky, requiring reasoning simultaneously about classical concurrent objects, which guarantee the atomicity of individual methods—the property known as linearizability—and about software-transactional-memory libraries, which guarantee the atomicity of user-defined sequences of method calls—or serializability. We present a formal-verification framework called C4, built up from the familiar notion of linearizability and its compositional properties, that allows proof of both kinds of libraries, along with composition of theorems from both styles to prove correctness of applications or further libraries. We apply the framework in a significant case study, verifying a transactional set object built out of both classical and transactional components following the technique of transactional predication; the proof is modular, reasoning separately about the transactional and nontransactional parts of the implementation. Central to our approach is the use of syntactic transformers on interaction trees—i.e., transactional libraries that transform client code to enforce particular synchronization disciplines. Our framework and case studies are mechanized in Coq.},
  journal = {Proc. ACM Program. Lang.},
  month = {apr},
  articleno = {80},
  numpages = {31},
  keywords = {concurrency, serializability, linearizability, verification, objects},
  plclub = {Yes},
  bcp = {Yes},
  keys = {verification}
}

@article{GoldsteinOOPSLA2022,
  author = {Goldstein, Harrison and Pierce, Benjamin C.},
  title = {Parsing Randomness},
  year = {2022},
  issue_date = {October 2022},
  number = {OOPSLA},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  journal = {Proc. ACM Program. Lang.},
  plclub = {Yes},
  bcp = {Yes},
  paper = {http://www.cis.upenn.edu/~bcpierce/papers/oopsla22.pdf},
  keys = {verification}
}

@inproceedings{10.1145/3491101.3503713,
  author = {J. Bietz, Matthew and Goyal, Nitesh and Immorlica, Nicole and MacIntyre, Blair and Monroy-Hern\'{a}ndez, Andr\'{e}s and C. Pierce, Benjamin and Rintel, Sean and Wohn, Donghee Yvette},
  title = {Social Presence in Virtual Event Spaces},
  year = {2022},
  isbn = {9781450391566},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  url = {https://doi.org/10.1145/3491101.3503713},
  doi = {10.1145/3491101.3503713},
  abstract = {It is generally acknowledged that the virtual event platforms of today do not perform satisfactorily at what is arguably their most important function: providing attendees with a sense of social presence. Social presence is the “sense of being with another” and can include ways of knowing who is in the virtual space, how others are reacting to what is happening in the space, an awareness of others’ activities and availability, and an idea of how to connect with them. Issues around presence and awareness have been perennial topics in the CHI and CSCW communities for decades. Nevertheless, the time feels ripe for a new effort with a special focus on larger-scale virtual events, given the accelerated pace of change in the socio-technological landscape and the tremendous potential impact that new insights could now have. The goal of this workshop is to bring together researchers and developers from academia and industry with a shared interest in improving the experience of virtual events to exchange insights and hopefully energize an ongoing community effort in this area.},
  booktitle = {CHI Conference on Human Factors in Computing Systems Extended Abstracts},
  articleno = {106},
  numpages = {5},
  keywords = {Virtual conventions, Virtual conferences, Virtual meetings, Awareness, Social presence},
  location = {New Orleans, LA, USA},
  series = {CHI EA '22},
  plclub = {Yes},
  bcp = {Yes},
  keys = {climate,misc}
}

@misc{Pierce:LambdaTA2022,
  author = {Benjamin C. Pierce},
  title = {Software Foundations, 15 years on},
  day = 20,
  month = jul,
  year = 2022,
  note = {Talk at Newton Institute workshop on Formal Education},
  plclub = {Yes},
  bcp = {Yes},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/LambdaTA-Newton.pdf},
  keys = {verification}
}

@misc{Pierce:ImaginingTheReader2023,
  author = {Benjamin C. Pierce},
  title = {Imagining the Reader},
  day = 20,
  month = jul,
  year = 2022,
  note = {Talk at Programming Languages Mentoring Workshop (PLMW)},
  plclub = {Yes},
  bcp = {Yes},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/PLMW2023-ImaginingTheReader.pdf},
  keys = {misc}
}

@inproceedings{Shi2023,
  author = {Jessica Shi and Benjamin Pierce and Andrew Head},
  title = {Towards a Science of Interactive Proof Reading},
  year = {2023},
  booktitle = {13th annual workshop on the intersection of HCI and PL (PLATEAU)},
  bcp = {Yes},
  plclub = {Yes},
  keys = {misc,verification}
}

@misc{cutler2023stream,
  title = {Stream Types},
  author = {Joseph W. Cutler and Christopher Watson and
              Phillip Hilliard and Harrison Goldstein and
              Caleb Stanford and Benjamin C. Pierce},
  year = {2023},
  eprint = {2307.09553},
  archiveprefix = {arXiv},
  primaryclass = {cs.PL},
  url = {https://arxiv.org/abs/2307.09553},
  bcp = {Yes},
  plclub = {Yes}
}

@article{shi2023etna,
  title = {Etna: An Evaluation Platform for Property-Based Testing
                  (Experience Report)},
  author = {Shi, Jessica and Keles, Alperen and Goldstein, Harrison
                  and Pierce, Benjamin C and Lampropoulos, Leonidas},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {7},
  number = {ICFP},
  pages = {878--894},
  year = {2023},
  bcp = {Yes},
  plclub = {Yes},
  paper = {http://www.cis.upenn.edu/~bcpierce/papers/etna2023.pdf},
  publisher = {ACM New York, NY, USA}
}

@misc{Pierce:Subtyping2023,
  author = {Benjamin C. Pierce},
  title = {What Does Subtyping Mean?},
  day = 4,
  month = aug,
  year = 2023,
  note = {Talk at Programming Languages Mentoring Workshop (PLMW)},
  plclub = {Yes},
  bcp = {Yes},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/2023-PLMW-Subtyping.pdf},
  keys = {types}
}

@inproceedings{Goldstein2024ICSE,
  title = {Property-Based Testing in Practice},
  author = {Harrison Goldstein and Joseph W. Cutler and
                  Daniel Dickstein and Benjamin C. Pierce and Andrew Head},
  year = {2024},
  booktitle = {International Conference on Software Engineering (ICSE)},
  url = {https://harrisongoldste.in/papers/icse24-pbt-in-practice.pdf},
  bcp = {Yes},
  plclub = {Yes}
}

@inproceedings{goldstein_property-based_2024,
  title = {Property-{Based} {Testing} in {Practice}},
  booktitle = {International {Conference} on {Software} {Engineering} ({ICSE})},
  author = {Goldstein, Harrison and Cutler, Joseph W and Dickstein, Daniel and Pierce, Benjamin C and Head, Andrew},
  year = {2024},
  url = {http://www.cis.upenn.edu/~bcpierce/papers/icse24-pbt-in-practice},
  bcp = {Yes},
  plclub = {Yes},
  keys = {testing}
}

@misc{Pierce:TFP24,
  author = {Benjamin C. Pierce},
  title = {delta: Ordered Types for Stream Processing},
  day = 10,
  month = jan,
  year = 2024,
  note = {Talk at Trends in Functional Programming (TFP)},
  plclub = {Yes},
  bcp = {Yes},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/2024-TFP-talk.pdf},
  keys = {types}
}

@misc{Pierce:POPL24ClimateTalk,
  author = {Benjamin C. Pierce},
  title = {},
  day = 17,
  month = jan,
  year = 2024,
  note = {Short talk at POPL reception},
  plclub = {Yes},
  bcp = {Yes},
  slides = {http://www.cis.upenn.edu/~bcpierce/papers/2024-POPL-reception-talk.pdf},
  keys = {climate}
}

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