Harrison Goldstein, Samantha Frohlich, Benjamin C. Pierce, and Meng Wang. Reflecting on Random Generation, February 2023. Under submission. [ bib ]

Jessica Shi, Benjamin Pierce, and Andrew Head. Towards a Science of Interactive Proof Reading. In 13th annual workshop on the intersection of HCI and PL (PLATEAU), 2023. [ bib ]

Harrison Goldstein, Samantha Frohlich, Meng Wang, and Benjamin C Pierce. Reflecting on Random Generation. Proceedings of the ACM on Programming Languages, 7(ICFP):322--355, 2023. [ bib ]

Benjamin C. Pierce. Software Foundations, 15 years on, July 2022. Talk at Newton Institute workshop on Formal Education. [ bib | slides ]

Benjamin C. Pierce. Understanding Property-Based Testing by Talking to People, May 2022. Short talk at Working Group 2.8. [ bib | slides ]

Benjamin C. Pierce. (When) Will Property-Based Testing Rule The World?, May 2022. Keynote at Yow! Lambda Jam Conference. [ bib | slides ]

Joseph Cutler, Harrison Goldstein, Koen Claessen, John Hughes, and Benjamin C. Pierce. Functional Pearl: Holey Generators!, May 2022. Draft. [ bib ]

Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, and Steve Zdancewic. C4: Verified Transactional Objects. Proc. ACM Program. Lang., 6(OOPSLA1), apr 2022. [ bib | DOI | DOI | pdf ]

Keywords: concurrency, serializability, linearizability, verification, objects

Mohsen Lesani, Li-Yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, and Steve Zdancewic. C4: Verified Transactional Objects. Proc. ACM Program. Lang., 6(OOPSLA1), apr 2022. [ bib | DOI | DOI | pdf ]

Keywords: objects, serializability, concurrency, verification, linearizability

Mohsen Lesani, Li-Yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, and Steve Zdancewic. Modular Mechanized Verification of Transactional Predication. Proc. ACM Program. Lang., 6(OOPSLA1), April 2022. OOPSLA 2022. [ bib ]

Li-Yao Xia. Executable Semantics with Interaction Trees. PhD thesis, University of Pennsylvania, 2022. [ bib | pdf ]

Yishuai Li. Testing By Dualization. PhD thesis, University of Pennsylvania, 2022. [ bib | pdf ]

Harrison Goldstein and Benjamin C. Pierce. Parsing Randomness. Proc. ACM Program. Lang., (OOPSLA), 2022. [ bib ]

Harrison Goldstein and Benjamin C. Pierce. Making Better Choices: Guiding Random Generators with Derivatives, 2022. Draft. [ bib ]

Harrison Goldstein and Benjamin C. Pierce. Parsing Randomness: Unifying and Differentiating Parsers and Random Generators. CoRR, abs/2203.00652, 2022. [ bib | DOI | arXiv | DOI | pdf ]

Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, William Mansky, Benjamin C. Pierce, and Steve Zdancewic. Verifying an HTTP Key-Value Server with Interaction Trees and VST. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference), volume 193 of LIPIcs, pages 32:1--32:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. [ bib | DOI | DOI | pdf ]

Sean Noble Anderson, Leonidas Lampropoulos, Roberto Blanco, Benjamin C. Pierce, and Andrew Tolmach. Security Properties for Stack Safety. CoRR, abs/2105.00417, 2021. [ bib | arXiv | pdf ]

Sean Noble Anderson, Leonidas Lampropoulos, Roberto Blanco, Benjamin C. Pierce, and Andrew Tolmach. Security Properties for Stack Safety. In Workshop on Foundations of Computer Security (FCS), 2021. [ bib ]

Harrison Goldstein, John Hughes, Leonidas Lampropoulos, and Benjamin C. Pierce. Do Judge a Test by its Cover: Combining Combinatorial and Property-Based Testing. In Nobuko Yoshida, editor, 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, volume 12648 of Lecture Notes in Computer Science, pages 264--291. Springer, 2021. [ bib | DOI | DOI | pdf ]

Yishuai Li, Benjamin C. Pierce, and Steve Zdancewic. Model-based testing of networked applications. In Cristian Cadar and Xiangyu Zhang, editors, ISSTA '21: 30th ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event, Denmark, July 11-17, 2021, pages 529--539. ACM, 2021. [ bib | DOI | DOI | pdf ]

Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang., 4(POPL):51:1--51:32, 2020. Distinguished paper award. [ bib | DOI | DOI | pdf ]

Benjamin C. Pierce. POPLmark 15 Year Retrospective Panel at Certified Programs and Proofs, 2020. Written up in https://blog.sigplan.org/2020/01/29/mechanized-proofs-for-pl-past-present-and-future/. [ bib | pdf ]

Leonidas Lampropoulos, Diane Gallois-Wong, Cătălin Hritcu, John Hughes, Benjamin C. Pierce, and Li-yao Xia. Beginner's Luck: A Language for Random Generators. In Gilles Barthe, Joost-Pieter Katoen, and Alexandra Silva, editors, Foundations of Programming and Software systems: Probabilistic Programming. 2020. An earlier version appeared in ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), Jan 2017. [ bib | pdf ]

Benjamin C. Pierce. The Science of Deep Specification, June 2019. Opening talk at DeepSpec workshop. [ bib | slides ]

Leonidas Lampropoulos, Michael Hicks, and Benjamin C. Pierce. Coverage guided, property based testing. Proc. ACM Program. Lang., 3(OOPSLA):181:1--181:29, 2019. [ bib | DOI | DOI | pdf ]

Leonidas Lampropoulos and Benjamin C. Pierce. QuickChick: Property-Based Testing in Coq. Software Foundations series, volume 4. Electronic textbook, August 2018. http://www.cis.upenn.edu/ bcpierce/sf. [ bib | book ]

Benjamin C. Pierce. Specifying the DeepSpec Web Server, June 2018. Talk at DeepSpec workshop. [ bib | slides ]

Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Catalin Hritcu, Vilhelm Sjöberg, Andrew Tolmach, and Brent Yorgey. Programming Language Foundations. Software Foundations series, volume 2. Electronic textbook, May 2018. Version 5.5. http://www.cis.upenn.edu/ bcpierce/sf. [ bib | japanese translation | book ]

Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Catalin Hritcu, Vilhelm Sjöberg, and Brent Yorgey. Logical Foundations. Software Foundations series, volume 1. Electronic textbook, May 2018. Version 5.5. http://www.cis.upenn.edu/ bcpierce/sf. [ bib | japanese translation | book ]

Benjamin C. Pierce. The Science of Deep Specification, April 2018. Invited keynote at ETAPS / POST. [ bib | video | slides ]

Leonidas Lampropoulos, Zoe Paraskevopoulou, and Benjamin C. Pierce. Generating good generators for inductive relations. PACMPL, 2(POPL):45:1--45:30, 2018. [ bib | DOI | DOI | short version | pdf ]

Arthur Azevedo de Amorim, Catalin Hritcu, and Benjamin C. Pierce. The Meaning of Memory Safety. In Lujo Bauer and Ralf Küsters, editors, 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, volume 10804 of Lecture Notes in Computer Science, pages 79--105. Springer, 2018. [ bib | DOI | DOI | pdf ]

Benjamin C. Pierce. The Science of Deep Specification, September 2017. WATCH lecture at NSF. [ bib ]

Andrew W. Appel, Lennart Beringer, Adam Chlipala, Benjamin C. Pierce, Zhong Shao, Stephanie Weirich, and Steve Zdancewic. Position paper: The science of deep specification. Philosophical Transactions of the Royal Society of London A: Mathematical, Physical and Engineering Sciences, 375(2104), 2017. [ bib | DOI | arXiv | DOI | pdf ]

Arthur Azevedo de Amorim, Cătălin Hritcu, and Benjamin C. Pierce. The Meaning of Memory Safety. In ACM Conference on Computer and Communications Security (CCS), 2017. Under submission. [ bib ]

Leonidas Lampropoulos, Diane Gallois-Wong, Cătălin Hritcu, John Hughes, Benjamin C. Pierce, and Li-yao Xia. Beginner's Luck: A Language for Random Generators. In 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), January 2017. [ bib | pdf ]

Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Catalin Hritcu, Vilhelm Sjöberg, and Brent Yorgey. Software Foundations. Electronic textbook, 2017. Version 5.0. http://www.cis.upenn.edu/ bcpierce/sf. [ bib | japanese translation | book ]

Benjamin C. Pierce. Interview with Markus Völter on The Science of Deep Specification for Omega Tau podcast, November 2016. [ bib | transcript ]

Benjamin C. Pierce. Interview with Tijs van der Storm on The Science of Deep Specification for release.nl magazine, November 2016. [ bib | transcript ]

Benjamin C. Pierce. The Science of Deep Specification, November 2016. Invited keynote at SPLASH / OOPSLA. [ bib | video | slides ]

Leonidas Lampropoulos, Diane Gallois-Wong, Cătălin Hritcu, John Hughes, Benjamin C. Pierce, and Li-yao Xia. Beginner's Luck: A Language for Random Generators. Draft, arXiv:1607.05443, July 2016. [ bib | pdf ]

Benjamin C. Pierce. The Science of Deep Specification, May 2016. High-Confidence Software Systems (HCSS). [ bib | slides ]

John Hughes, Benjamin C. Pierce, Thomas Arts, and Ulf Norell. Mysteries of Dropbox: Property-Based Testing of a Distributed Synchronization Service. In International Conference on Software Testing, Verification and Validation (ICST), April 2016. [ bib | short version | slides ]

Zoe Paraskevopoulou, Cătălin Hritcu, Maxime Dénès, Leonidas Lampropoulos, and Benjamin C. Pierce. Foundational Property-Based Testing. In International Conference on Interactive Theorem Proving (ITP), 2015. [ bib ]

Maxime Dénès, Catalin Hritcu, Leonidas Lampropoulos, Zoe Paraskevopoulou, and Benjamin C. Pierce. QuickChick: Property-Based Testing for Coq (abstract). In VSL, 2014. [ bib | pdf ]

Cătălin Hritcu, John Hughes, Benjamin C. Pierce, Antal Spector-Zabusky, Dimitrios Vytiniotis, Arthur Azevedo de Amorim, and Leonidas Lampropoulos. Testing Noninterference, Quickly. In 18th ACM SIGPLAN International Conference on Functional Programming (ICFP), September 2013. 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. [ bib | pdf ]

Benjamin C. Pierce. Proof Assistant as Teaching Assistant: A View from the Trenches, July 2010. Keynote address at International Conference on Interactive Theorem Proving (ITP). [ bib | slides ]

Benjamin C. Pierce. Lambda, The Ultimate TA: Using a Proof Assistant to Teach Programming Language Foundations, September 2009. Keynote address at International Conference on Functional Programming (ICFP). [ bib | slides ]

Benjamin C. Pierce. Using a Proof Assistant to Teach Programming Language Foundations, or, Lambda, the Ultimate TA, April 2008. White paper. [ bib | short version ]

Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich. Engineering formal metatheory. In ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages (POPL), San Francisco, California, pages 3--15. ACM, January 2008. [ bib | short version ]

Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich. Engineering Formal Metatheory, July 2007. Submitted for publication. [ bib | short version ]

Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized metatheory for the masses: The POPLmark Challenge. In International Conference on Theorem Proving in Higher Order Logics (TPHOLs), August 2005. [ bib | pdf | .ps ]