Benjamin Pierce's Publications

Books

Specification, Verification, and Testing

Security and Privacy

Bidirectional Programming (Lenses)

File and Data Synchronization

Static Types for XML Processing
      Xtatic
      XDuce

Concurrent and Distributed Systems
      Mobile Agents
      Pi-Calculus and Pict

Types
      Surveys
      Contracts
      Modular Type Systems
      Type Inference
      Object-Oriented Programming
      Subtyping
      Intersection and Union Types
      Extensible Records
      Dynamic Types
      Semantics

Climate Change

Miscellaneous

Bibliography

All publications, chronologically

Recent Activities

Benjamin C. Pierce, January 2024. Short talk at POPL reception. [ bib | slides ]

Benjamin C. Pierce. delta: Ordered Types for Stream Processing, January 2024. Talk at Trends in Functional Programming (TFP). [ bib | slides ]

Harrison Goldstein, Joseph W Cutler, Daniel Dickstein, Benjamin C Pierce, and Andrew Head. Property-Based Testing in Practice. In International Conference on Software Engineering (ICSE), 2024. [ bib | pdf ]

Harrison Goldstein, Joseph W. Cutler, Daniel Dickstein, Benjamin C. Pierce, and Andrew Head. Property-Based Testing in Practice. In International Conference on Software Engineering (ICSE), 2024. [ bib | pdf ]

Benjamin C. Pierce. What Does Subtyping Mean?, August 2023. Talk at Programming Languages Mentoring Workshop (PLMW). [ bib | slides ]

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

Jessica Shi, Alperen Keles, Harrison Goldstein, Benjamin C Pierce, and Leonidas Lampropoulos. Etna: An Evaluation Platform for Property-Based Testing (Experience Report). Proceedings of the ACM on Programming Languages, 7(ICFP):878--894, 2023. [ bib ]

Joseph W. Cutler, Christopher Watson, Phillip Hilliard, Harrison Goldstein, Caleb Stanford, and Benjamin C. Pierce. Stream Types, 2023. [ bib | arXiv | pdf ]

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 ]

Sean Noble Anderson, Leonidas Lampropoulos, Roberto Blanco, Benjamin C. Pierce, and Andrew Tolmach. Stack Safety as a Security Property. In IEEE Symposium on Computer Security Foundations (CSF). IEEE Computer Society Press, 2023. [ bib ]

Benjamin C. Pierce. Imagining the Reader, July 2022. Talk at Programming Languages Mentoring Workshop (PLMW). [ bib | slides ]

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 ]

Matthew J. Bietz, Nitesh Goyal, Nicole Immorlica, Blair MacIntyre, Andrés Monroy-Hernández, Benjamin C. Pierce, Sean Rintel, and Donghee Yvette Wohn. Social Presence in Virtual Event Spaces. In CHI Conference on Human Factors in Computing Systems Extended Abstracts, CHI EA '22, New York, NY, USA, 2022. Association for Computing Machinery. [ bib | DOI | DOI | pdf ]

Keywords: Virtual conventions, Virtual conferences, Virtual meetings, Awareness, Social presence

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 ]

Derek Dreyer and Benjamin C. Pierce. On being a PhD student of Robert Harper. Journal of Functional Programming, 32.32, 2022. [ 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 ]

Matthew J. Bietz, Nitesh Goyal, Nicole Immorlica, Blair MacIntyre, Andrés Monroy-Hernández, Benjamin C. Pierce, Sean Rintel, and Donghee Yvette Wohn. Social Presence in Virtual Event Spaces. In Simone D. J. Barbosa, Cliff Lampe, Caroline Appert, and David A. Shamma, editors, 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. ACM, 2022. [ bib | DOI | DOI | pdf ]

A complete list of publications, in chronological order, can be found here.

Bibliography

My BibTeX database includes canonical citations for all of the following papers and books.

Books

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, 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, 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, editor. Advanced Topics in Types and Programming Languages. MIT Press, 2005. [ bib | home page ]

Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002. [ bib | errata | home page ]

Benjamin C. Pierce. Basic Category Theory for Computer Scientists. MIT Press, 1991. [ bib ]

Specification, Verification, and Testing:

Visit the DeepSpec home page!

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 ]

Keywords: concurrency, serializability, linearizability, verification, objects

Keywords: objects, serializability, concurrency, verification, linearizability

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 ]

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

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. 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 ]

Visit the PoplMark Challenge home page!

Security and Privacy:

Visit the CRASH/SAFE home page!

Visit the Penn Privacy group home page!

Hengchu Zhang, Edo Roth, Andreas Haeberlen, Benjamin C. Pierce, and Aaron Roth. Testing Differential Privacy with Dual Interpreters. Proc. ACM Program. Lang., (OOPSLA), 2020. [ bib ]

Hengchu Zhang, Edo Roth, Andreas Haeberlen, Benjamin C. Pierce, and Aaron Roth. Fuzzi: a three-level logic for differential privacy. Proc. ACM Program. Lang., 3(ICFP):93:1--93:28, 2019. [ bib | DOI | DOI | pdf ]

Carmine Abate, Arthur Azevedo de Amorim, Roberto Blanco, Ana Nora Evans, Guglielmo Fachini, Catalin Hritcu, Théo Laurent, Benjamin C Pierce, Marco Stronati, and Andrew Tolmach. When good components go bad: Formally secure compilation despite dynamic compromise. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, pages 1351--1368. ACM, 2018. [ bib ]

Daniel Winograd-Cord, Andreas Haeberlen, Aaron Roth, and Benjamin C. Pierce. A Framework for Adaptive Differential Privacy. In ACM SIGPLAN International Conference on Functional Programming (ICFP), September 2017. [ bib ]

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 ]

Daniel Winograd-Cord, Andreas Haeberlen, Aaron Roth, and Benjamin C. Pierce. A Framework for Adaptive Differential Privacy, July 2016. Submitted to POPL 2017. [ bib ]

Yannis Juglaret, Cătălin Hritcu, Arthur Azevedo de Amorim, Boris Eng, and Benjamin C. Pierce. Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation. In 29th IEEE Symposium on Computer Security Foundations (CSF). IEEE Computer Society Press, July 2016. arXiv:1602.04503. [ bib | pdf ]

Daniel Schoepe, Musard Balliu, Benjamin C. Pierce, and Andrei Sabelfeld. Explicit Secrecy: A Policy for Taint Tracking. In IEEE European Symposium on Security and Privacy, EuroS&P 2016, Saarbrücken, Germany, March 21-24, 2016, pages 15--30. IEEE, 2016. [ bib | DOI | DOI | pdf ]

Gilles Barthe, Marco Gaboardi, Justin Hsu, and Benjamin C Pierce. Programming language techniques for differential privacy. ACM SIGLOG News, 3(1):34--53, January 2016. [ bib | pdf ]

Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Cătălin Hritcu, Benjamin C. Pierce, Antal Spector-Zabusky, and Andrew Tolmach. Micro-Policies: Formally Verified, Tag-Based Security Monitors. In 36th IEEE Symposium on Security and Privacy (Oakland S&P). IEEE, May 2015. [ bib | short version | slides ]

Udit Dhawan, Cătălin Hritcu, Rafi Rubin, Nikos Vasilakis, Silviu Chiricescu, Jonathan M. Smith, Thomas F. Knight, Jr., Benjamin C. Pierce, and André DeHon. Architectural Support for Software-Defined Metadata Processing, 2015. [ bib | pdf ]

Benjamin C. Pierce. Micro-Policies: A Framework for Tag-Based Security Monitors, December 2014. Distinguished Lecture at University of Minnesota. [ bib | slides ]

Benjamin C. Pierce. Interview with Luke Muehlhauser on Clean-Slate Security Architectures for Machine Intelligence Research Institute blog, May 2014. [ bib | transcript ]

Benjamin C. Pierce. Programmable Hardware Support for Ubiquitous Micro-Policy Enforcement, May 2014. Talk at High-Confidence Software Systems. [ bib | slides ]

Benjamin C. Pierce. Principles, Meet Practice: An Early Retrospective on SAFE, January 2014. Talk at Principles in Practice Workshop (PiP). [ bib | slides ]

Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Cătălin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, and Andrew Tolmach. A Verified Information-Flow Architecture. In Proceedings of the 41st Symposium on Principles of Programming Languages, POPL, January 2014. Full version in Journal of Computer Security, Special Issue on Verified Information Flow Security, Dec 2016. [ bib | pdf | full version ]

Justin Hsu, Marco Gaboardi, Andreas Haeberlen, Sanjeev Khanna, Arjun Narayan, Benjamin C. Pierce, and Aaron Roth. Differential Privacy: An Economic Method for Choosing Epsilon. In Computer Security Foundations Symposium (CSF), 2014. [ bib | pdf ]

Udit Dhawan, Nikos Vasilakis, Raphael Rubin, Silviu Chiricescu, Jonathan M. Smith, Thomas F. Knight, Benjamin C. Pierce, and André DeHon. PUMP -- A Programmable Unit for Metadata Processing. In Proceedings of the 3rd International Workshop on Hardware and Architectural Support for Security and Privacy, HASP '14, New York, NY, USA, 2014. ACM. [ bib | DOI | DOI | pdf ]

Silviu Chiricescu, André DeHon, Delphine Demange, Suraj Iyer, Aleksey Kliger, Greg Morrisett, Benjamin C. Pierce, Howard Reubenstein, Jonathan M. Smith, Gregory T. Sullivan, Arun Thomas, Jesse Tov, Christopher M. White, and David Wittenberg. SAFE: A Clean-Slate Architecture for Secure Systems. In Proceedings of the IEEE International Conference on Technologies for Homeland Security, November 2013. [ bib ]

Benjamin C. Pierce. The SAFE Machine: An Architecture for Pervasive Information Flow, June 2013. Invited talk at Computer Security Foundations Symposium (CSF). [ bib | slides ]

Benoît Montagu, Benjamin C. Pierce, and Randy Pollack. A Theory of Information-Flow Labels. In Proceedings of the 2013 IEEE Computer Security Foundations Symposium, June 2013. [ bib | coq code | short version ]

Cătălin Hritcu, Michael Greenberg, Ben Karel, Benjamin C. Pierce, and Greg Morrisett. All Your IFCException Are Belong To Us. In 34th IEEE Symposium on Security and Privacy (Oakland), May 2013. [ bib | short version ]

Marco Gaboardi, Andreas Haeberlen, Justin Hsu, Arjun Narayan, and Benjamin C. Pierce. Linear Dependent Types for Differential Privacy. In ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages (POPL), Rome, Italy, January 2013. [ bib | short version ]

Benjamin C. Pierce. Differential Privacy in the Programming Languages Community, October 2012. Invited tutorial at DIMACS Workshop on Recent Work on Differential Privacy across Computer Science. [ bib | video | slides ]

Benjamin C. Pierce. Verification Challenges of Pervasive Information Flow, January 2012. Invited talk at Programming Languages Meets Program Verification workshop (PLPV). [ bib | slides ]

André DeHon, Ben Karel, Thomas F. Knight, Jr., Gregory Malecha, Benoît Montagu, Robin Morisset, Greg Morrisett, Benjamin C. Pierce, Randy Pollack, Sumit Ray, Olin Shivers, Jonathan M. Smith, and Gregory Sullivan. Preliminary Design of the SAFE Platform. In 6th Workshop on Programming Languages and Operating Systems, PLOS, October 2011. [ bib | pdf ]

Andreas Haeberlen, Benjamin C. Pierce, and Arjun Narayan. Differential Privacy Under Fire. In Proceedings of the 20th USENIX Security Symposium, August 2011. [ bib | pdf ]

Jason Reed and Benjamin C. Pierce. Distance Makes the Types Grow Stronger: A Calculus for Differential Privacy. In ACM SIGPLAN International Conference on Functional Programming (ICFP), Baltimore, Maryland, September 2010. [ bib | short version ]

Aaron Bohannon and Benjamin C. Pierce. Featherweight Firefox: Formalizing the Core of a Web Browser. In Usenix Conference on Web Application Development (WebApps), June 2010. [ bib | short version ]

Jason Reed, Adam J. Aviv, Daniel Wagner, Andreas Haeberlen, Benjamin C. Pierce, and Jonathan M. Smith. Differential Privacy for Collaborative Security. In European Workshop on System Security (EUROSEC), April 2010. [ bib | manuscript ]

Aaron Bohannon, Benjamin C. Pierce, Vilhelm Sjöberg, Stephanie Weirich, and Steve Zdancewic. Reactive Noninterference. In CCS '09: Proceedings of the 16th ACM conference on Computer and communications security, pages 79--90, New York, NY, USA, 2009. ACM. [ bib | DOI | DOI ]

Karl Crary, Robert Harper, Frank Pfenning, Benjamin C. Pierce, Stephanie Weirich, and Stephan Zdancewic. Manifest Security. White paper, January 2007. [ bib | pdf ]

Karl Crary, Robert Harper, Frank Pfenning, Benjamin C. Pierce, Stephanie Weirich, and Stephan Zdancewic. Manifest Security for Distributed Information. White paper, March 2006. [ bib | pdf ]

Eijiro Sumii and Benjamin C. Pierce. A Bisimulation for Type Abstraction and Recursion. In ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages (POPL), Long Beach, California, 2005. Full version in J. ACM, 54 (5), 2007. [ bib | short version | full version ]

Eijiro Sumii and Benjamin C. Pierce. A Bisimulation for Dynamic Sealing. In ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages (POPL), Venice, Italy, 2004. Full version in Theoretical Computer Science 375 (2007), 169--192. [ bib | conference version ]

Eijiro Sumii and Benjamin C. Pierce. Logical Relations for Encryption. Journal of Computer Security, 11(4):521--554, 2003. Extended abstract appeared in ph14th IEEE Computer Security Foundations Workshop, pp. 256--269, 2001. [ bib | conference version ]

Benjamin Pierce and Eijiro Sumii. Relating Cryptography and Polymorphism, July 2000. Some parts superseded by [41] (Sumii and Pierce, 2001). [ bib | manuscript ]

Bidirectional Programming (Lenses):

Visit the Boomerang home page!

Anders Miltner, Solomon Maina, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic. Synthesizing symmetric lenses. Proc. ACM Program. Lang., 3(ICFP):95:1--95:28, 2019. [ bib | DOI | DOI | pdf ]

Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic. Synthesizing Bijective Lenses. Proceedings of the ACM on Programming Languages (PACMPL), January 2018. [ bib | short version ]

Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic. Synthesizing bijective lenses. PACMPL, 2(POPL):1:1--1:30, 2018. [ bib | DOI | DOI | short version | pdf ]

Benjamin C. Pierce. A Deep Specification for Dropbox, November 2015. Keynote address at Clojure/conj. [ bib | video | slides ]

Martin Hofmann, Benjamin C. Pierce, and Daniel Wagner. Symmetric Lenses. Journal of the ACM, 2015. To appear; extended abstract in POPL 2011. [ bib | short version ]

Benjamin C. Pierce. Mysteries of Dropbox, November 2014. Keynote address at CERN Workshop on Cloud Services for File Synchronisation and Sharing. [ bib | video | slides ]

Daniel Wagner. Symmetric Edit Lenses: A New Foundation for Bidirectional Languages. PhD thesis, University of Pennsylvania, 2014. [ bib | pdf ]

Martin Hofmann, Benjamin C. Pierce, and Daniel Wagner. Edit languages for information trees. In Second International Workshop on Bidirectional Transformations (BX), April 2013. [ bib ]

Udit Dhawan, Albert Kwon, Edin Kadric, Cătălin Hritcu, Benjamin C. Pierce, Jonathan M. Smith, Gregory Malecha, Greg Morrisett, Thomas F. Knight, Jr., Andrew Sutherland, Tom Hawkins, Amanda Zyxnfryx, David Wittenberg, Peter Trei, Sumit Ray, Greg Sullivan, and André DeHon. Hardware Support for Safety Interlocks and Introspection. In SASO Workshop on Adaptive Host and Network Security, September 2012. [ bib | pdf ]

Benjamin C. Pierce. Linguistic Foundations for Bidirectional Transformations, May 2012. Invited tutorial at Principles of Database Systems (PODS). [ bib | slides ]

Martin Hofmann, Benjamin C. Pierce, and Daniel Wagner. Edit Lenses. In ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages (POPL), Philadelphia, Pennsylvania, January 2012. [ bib | short version | slides ]

Martin Hofmann, Benjamin C. Pierce, and Daniel Wagner. Symmetric Lenses. In ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages (POPL), Austin, Texas, January 2011. [ bib | short version | full version ]

Davi M. J. Barbosa, Julien Cretin, Nate Foster, Michael Greenberg, and Benjamin C. Pierce. Matching Lenses: Alignment and View Update. In ACM SIGPLAN International Conference on Functional Programming (ICFP), Baltimore, Maryland, September 2010. [ bib | tech report | short version ]

Benjamin C. Pierce. Foundations for Bidirectional Programming, or: How To Build a Bidirectional Programming Language, June 2009. Keynote address at International Conference on Model Transformation (ICMT). [ bib | slides ]

J. Nathan Foster, Alexandre Pilkiewicz, and Benjamin C. Pierce. Quotient Lenses. In ACM SIGPLAN International Conference on Functional Programming (ICFP), Victoria, Canada, September 2008. [ bib | short version ]

Aaron Bohannon, J. Nathan Foster, Benjamin C. Pierce, Alexandre Pilkiewicz, and Alan Schmitt. Boomerang: Resourceful Lenses for String Data. In ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages (POPL), San Francisco, California, January 2008. [ bib | tech report | short version ]

Benjamin C. Pierce. Adventures in Bi-Directional Programming, December 2007. FSTTCS invited talk. [ bib | slides ]

Aaron Bohannon, J. Nathan Foster, Benjamin C. Pierce, Alexandre Pilkiewicz, and Alan Schmitt. Boomerang: Resourceful Lenses for String Data. Technical report, Dept. of CIS, University of Pennsylvania, July 2007. [ bib | tech report | short version ]

J. Nathan Foster, Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce, and Alan Schmitt. Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem. ACM Transactions on Programming Languages and Systems, 29(3):17, May 2007. Preliminary version presented at the Workshop on Programming Language Technologies for XML (PLAN-X), 2004; extended abstract presented at Principles of Programming Languages (POPL), 2005. [ bib | DOI | electronic appendix | DOI | conference version | full version | slides ]

J. Nathan Foster, Benjamin C. Pierce, and Alan Schmitt. A Logic Your Typechecker Can Count On: Unordered Tree Types in Practice. In Workshop on Programming Language Technologies for XML (PLAN-X), informal proceedings, January 2007. [ bib | conference version | slides ]

J. Nathan Foster, Michael B. Greenwald, Christian Kirkegaard, Benjamin C. Pierce, and Alan Schmitt. Exploiting Schemas in Data Synchronization. Journal of Computer and System Sciences, 73(4):669--689, 2007. Extended abstract in Database Programming Languages (DBPL) 2005. [ bib | tech report | short version | full version | slides ]

Benjamin C. Pierce. The Weird World of Bi-Directional Programming, March 2006. ETAPS invited talk. [ bib | slides ]

Aaron Bohannon, Jeffrey A. Vaughan, and Benjamin C. Pierce. Relational Lenses: A Language for Updateable Views. In Principles of Database Systems (PODS), 2006. Extended version available as University of Pennsylvania technical report MS-CIS-05-27. [ bib | tech report | pdf ]

Aaron Bohannon, Jeffrey A. Vaughan, and Benjamin C. Pierce. Relational Lenses: A Language for Updateable Views. Technical Report MS-CIS-05-27, Dept. of Computer and Information Science, University of Pennsylvania, December 2005. [ bib | pdf ]

Aaron Bohannon, Jeffrey A. Vaughan, and Benjamin C. Pierce. Relational Lenses: A language for defining updateable views, October 2005. Poster presented at Greater Philadelphia DB/IR Day. [ bib | pdf ]

Benjamin C. Pierce. Combinators for Bi-Directional Tree Transformations: A Linguistic Approach to the View Update Problem, October 2004. Invited talk at New England Programming Languages Symposium. [ bib | slides ]

Climate Change:

Benjamin C. Pierce, January 2024. Short talk at POPL reception. [ bib | slides ]

Keywords: Virtual conventions, Virtual conferences, Virtual meetings, Awareness, Social presence

Matthew J. Bietz, Nitesh Goyal, Nicole Immorlica, Blair MacIntyre, Andrés Monroy-Hernández, Benjamin C. Pierce, Sean Rintel, and Donghee Yvette Wohn. Social Presence in Virtual Event Spaces. In Simone D. J. Barbosa, Cliff Lampe, Caroline Appert, and David A. Shamma, editors, 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. ACM, 2022. [ bib | DOI | DOI | pdf ]

Crista Videira Lopes, Jeanna Matthews, and Benjamin Pierce. Best Practices for Planning Virtual Conferences, May 2020. Northstar Meetings Group blog, https://www.northstarmeetingsgroup.com/Planning-Tips-and-Trends/Event-Planning/Event-Technology/Navigating-New-World-Virtual-Digital-Conferences-in-COVID19-ACM. [ bib ]

ACM Presidential Task Force on What Conferences Can Do to Replace Face to Face Meetings (co-chairs, Crista Lopes and Jeanna Matthews; executive editor, Benjamin C. Pierce). Virtual Conferences: A Guide to Best Practices, May 2020. https://www.acm.org/virtual-conferences. [ bib ]

Benjamin C. Pierce, Michael Hicks, Crista Lopes, and Jens Palsberg. Conferences in an era of expensive carbon. Commun. ACM, 63(3):35--37, 2020. [ bib | DOI | DOI | pdf ]

Michael W. Hicks, Crista Lopes, Jens Palsberg, and Benjamin C. Pierce. SIGPLAN and Climate Change: A report from the SIGPLAN committee on climate change, September 2018. [ bib | video | slides in Keynote format | slides ]

Richard Kim and Benjamin C. Pierce. Carbon Offsets: An Overview for Scientific Societies, June 2018. Version 1.2. [ bib | pdf ]

Michael W. Hicks, Crista Lopes, Jens Palsberg, and Benjamin C. Pierce. SIGPLAN and Climate Change: A report from SIGPLAN's ad hoc committee on climate change, June 2018. [ bib | video | slides in Keynote format | slides ]

Michael W. Hicks, Crista Lopes, and Benjamin C. Pierce. Engaging with Climate Change: Some Possible Steps for SIGPLAN (Preliminary Report of the SIGPLAN Climate Committee, Version 1.2), June 2018. [ bib | pdf ]

Clowdr CIC. Midspace: An open-source platform for virtual academic conferences, 2020--2022. http://midspace.app. [ bib ]

Synchronization

Visit the Unison home page!

Sanjeev Khanna, Keshav Kunal, and Benjamin C. Pierce. A Formal Investigation of Diff3. In Arvind and Prasad, editors, Foundations of Software Technology and Theoretical Computer Science (FSTTCS), December 2007. [ bib | short version ]

Michael B. Greenwald, Sanjeev Khanna, Keshav Kunal, Benjamin C. Pierce, and Alan Schmitt. Agreeing to Agree: Conflict Resolution for Optimistically Replicated Data. In Shlomi Dolev, editor, International Symposium on Distributed Computing (DISC), 2006. [ bib | tech report | short version | slides ]

Benjamin C. Pierce. Harmony: The Art of Reconciliation, April 2005. Invited talk at Trusted Global Computing conference, April 2005. [ bib | slides ]

J. Nathan Foster, Michael B. Greenwald, Christian Kirkegaard, Benjamin C. Pierce, and Alan Schmitt. Schema-Directed Data Synchronization. Technical Report MS-CIS-05-02, University of Pennsylvania, March 2005. Supersedes MS-CIS-03-42. [ bib | tech report ]

Benjamin C. Pierce and Jérôme Vouillon. What's in Unison? A Formal Specification and Reference Implementation of a File Synchronizer. Technical Report MS-CIS-03-36, Dept. of Computer and Information Science, University of Pennsylvania, 2004. [ bib | tech report ]

Benjamin C. Pierce. Harmony: A Synchronization Framework for Tree-Structured Data, September 2003. Slides from a talk presented in several places (Cambridge, Edinburgh, Philadelphia, Princeton) in Fall 2003. [ bib | slides ]

Benjamin C. Pierce, Alan Schmitt, and Michael B. Greenwald. Bringing Harmony to Optimism: A Synchronization Framework for Heterogeneous Tree-Structured Data. Technical Report MS-CIS-03-42, University of Pennsylvania, 2003. Superseded by MS-CIS-05-02. [ bib | tech report ]

Benjamin C. Pierce. Synchronize globally, compute locally, July 2002. Keynote address at Research Day on Global Computing, EFPL, Lausanne. [ bib | slides ]

Benjamin C. Pierce. Unison: A file synchronizer and its specification, 2001. Invited talk at Theoretical Aspects of Computer Software (TACS), Sendai, Japan. [ bib | slides ]

Benjamin C. Pierce. File Synchronization: Theory and Practice, 2001. [ bib | slides ]

S. Balasubramaniam and Benjamin C. Pierce. What is a file synchronizer? In Fourth Annual ACM/IEEE International Conference on Mobile Computing and Networking (MobiCom '98), October 1998. Full version available as Indiana University CSCI technical report #507, April 1998. [ bib | tech report | conference version | slides ]

Native XML Processing in Statically Typed Languages

Xtatic

Visit the Xtatic home page!

Vladimir Gapeyev, François Garillot, and Benjamin C. Pierce. Statically Typed Document Transformation: An Xtatic Experience. In Workshop on Programming Language Technologies for XML (PLAN-X), informal proceedings, January 2006. Available from the Xtatic web site. [ bib | tech report | pdf ]

Michael Y. Levin and Benjamin C. Pierce. Type-based Optimization for Regular Patterns. In Database Programming Languages (DBPL), August 2005. [ bib | tech report ]

Vladimir Gapeyev, Michael Y. Levin, Benjamin C. Pierce, and Alan Schmitt. XML Goes Native: Run-time Representations for Xtatic. In 14th International Conference on Compiler Construction, April 2005. [ bib | tech report | conference version ]

Benjamin C. Pierce. Fancy Types for XML: Friend or Foe?, April 2005. Talk at LINKS workshop, April 2005. [ bib | slides ]

Vladimir Gapeyev, Michael Y. Levin, Benjamin C. Pierce, and Alan Schmitt. The Xtatic Experience. In Workshop on Programming Language Technologies for XML (PLAN-X), January 2005. University of Pennsylvania Technical Report MS-CIS-04-24, Oct 2004. [ bib | tech report | slides ]

Michael Y. Levin. Run, Xtatic, Run: Efficient Implementation of an Object-Oriented Language with Regular Pattern Matching. PhD thesis, University of Pennsylvania, 2005. [ bib | pdf ]

Vladimir Gapeyev, Michael Y. Levin, Benjamin C. Pierce, and Alan Schmitt. The Xtatic Compiler and Runtime System, 2005. [ bib | source code ]

Vladimir Gapeyev and Benjamin C. Pierce. Paths into Patterns. Technical Report MS-CIS-04-25, University of Pennsylvania, October 2004. [ bib | tech report ]

Benjamin C. Pierce. Native XML Processing in a Statically Typed Language: A Progress Report on the Xtatic Project, March 2004. [ bib | slides ]

Alan Schmitt. Native XML Processing in Object-Oriented Languages: Calling XMHell from PurgatOOry. In International Workshop on Foundations of Object-Oriented Languages (FOOL), informal proceedings, January 2004. Invited talk. [ bib | slides ]

Michael Y. Levin and Benjamin C. Pierce. Typed-based optimization for Regular Patterns. In First International Workshop on High Performance XML Processing, 2004. [ bib | short version | pdf | slides ]

Michael Y. Levin. Compiling Regular Patterns. In ACM SIGPLAN International Conference on Functional Programming (ICFP), Uppsala, Sweden, 2003. [ bib | conference version ]

Vladimir Gapeyev and Benjamin C. Pierce. Regular Object Types. In European Conference on Object-Oriented Programming (ECOOP), Darmstadt, Germany, 2003. A preliminary version was presented at FOOL '03. [ bib | short version | slides ]

XDuce

Véronique Benzaken, Giuseppe Castagna, Haruo Hosoya, Benjamin C. Pierce, and Stijn Vansummeren. XML Typechecking. In Encyclopedia of Database Systems. Springer, 2009. [ bib ]

Haruo Hosoya, Jérôme Vouillon, and Benjamin C. Pierce. Regular Expression Types for XML. ACM Transactions on Programming Languages and Systems (TOPLAS), 27(1):46--90, January 2005. Preliminary version in ICFP 2000. [ bib | conference version | full version ]

Haruo Hosoya and Benjamin C. Pierce. XDuce: A Statically Typed XML Processing Language. ACM Transactions on Internet Technology, 3(2):117--148, May 2003. [ bib | official version ]

Haruo Hosoya and Benjamin C. Pierce. Regular Expression Pattern Matching. In ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages (POPL), London, England, 2001. Full version in Journal of Functional Programming, 13(6), Nov. 2003, pp. 961--1004. [ bib | full version ]

Haruo Hosoya and Benjamin C. Pierce. XDuce: A Typed XML Processing Language (Preliminary Report). In Dan Suciu and Gottfried Vossen, editors, International Workshop on the Web and Databases (WebDB), May 2000. Reprinted in The Web and Databases, Selected Papers, Springer LNCS volume 1997, 2001. [ bib | conference version ]

Haruo Hosoya, Jérôme Vouillon, and Benjamin C. Pierce. Regular Expression Types for XML. In International Conference on Functional Programming (ICFP), 2000. [ bib | conference version ]

Peter Buneman and Benjamin Pierce. Union Types for Semistructured Data. In Internet Programming Languages. Springer-Verlag, September 1998. Proceedings of the International Database Programming Languages Workshop. LNCS 1686. [ bib | conference version ]

Concurrent and Distributed Systems

Survey talks:

Benjamin C. Pierce. Global Computing: Some Questions for FOOLs, 2001. Invited talk at FOOL workshop. [ bib | slides ]

Benjamin C. Pierce. Type Systems for Concurrent Calculi, 1998. Invited tutorial at CONCUR. [ bib | slides ]

Mobile Agents

Benjamin C. Pierce, Alessandro Romanel, and Daniel Wagner. The Spider Calculus: Computing in Active Graphs, 2010. Manuscript, available from http://www.cis.upenn.edu/ bcpierce/papers/spider_calculus.pdf. [ bib | manuscript ]

Peter Sewell, Pawel Wojciechowski, and Benjamin Pierce. Location Independence for Mobile Agents. In H. E. Bal, B. Belkhouche, and L. Cardelli, editors, Proceedings of ICCL '98, volume 1686 of lncs. Springer-Verlag, September 1999. An earlier version with title Location-Independent Communication for Mobile Agents: a Two-Level Architecture appeared as Technical Report 462, Computer Laboratory, University of Cambridge, April 1999. [ bib | tech report | official version ]

Pi-Calculus and Pict

Benjamin C. Pierce and David N. Turner. The Pict Programming Language, 2001. This directory contains various papers, including a tutorial and user's manual, as well as complete compiler sources and installation instructions. (Be sure not to miss the artwork department!). [ bib | home page ]

Benjamin C. Pierce and David N. Turner. Pict: A Programming Language Based on the Pi-Calculus. In Gordon Plotkin, Colin Stirling, and Mads Tofte, editors, Proof, Language and Interaction: Essays in Honour of Robin Milner, pages 455--494. MIT Press, 2000. [ bib | full version ]

Naoki Kobayashi, Benjamin C. Pierce, and David N. Turner. Linearity and the Pi-Calculus. ACM Transactions on Programming Languages and Systems, 21(5):914--947, September 1999. Summary in POPL 1996. [ bib | full version ]

Benjamin Pierce and Davide Sangiorgi. Behavioral Equivalence in the Polymorphic Pi-Calculus. In Principles of Programming Languages (POPL), pages 531--584, 1997. Full version in Journal of the Association for Computing Machinery (JACM), 47(3), May 2000. [ bib | full version ]

Uwe Nestmann and Benjamin C. Pierce. Decoding Choice Encodings. In Proceedings of CONCUR '96, August 1996. Full version in Information and Computation, 163(1): 1--59 (2000). [ bib | full version ]

Benjamin C. Pierce. Foundational Calculi for Programming Languages. In Allen B. Tucker, editor, Handbook of Computer Science and Engineering, chapter 139. CRC Press, 1996. [ bib | full version ]

Benjamin C. Pierce and David N. Turner. Concurrent Objects in a Process Calculus. In Takayasu Ito and Akinori Yonezawa, editors, Theory and Practice of Parallel Programming (TPPP), Sendai, Japan (Nov. 1994), number 907 in Lecture Notes in Computer Science, pages 187--215. Springer-Verlag, April 1995. [ bib | short version | pdf ]

Benjamin C. Pierce and Davide Sangiorgi. Typing and Subtyping for Mobile Processes. In Logic in Computer Science, 1993. Full version in Mathematical Structures in Computer Science , Vol. 6, No. 5, 1996. [ bib | full version ]

Types

Surveys:

Benjamin C. Pierce. Types à la Milner, April 2012. Talk at Philly Emerging Technologies Conference. [ bib | video ]

Benjamin C. Pierce. Types à la Milner, April 2012. Invited talk at Milner Symposium. [ bib | slides ]

Benjamin C. Pierce. Types, January 2012. Invited talk at Programming Languages Mentoring Workshop. [ bib | slides ]

Benjamin C. Pierce. Types Considered Harmful, May 2008. Invited talk at Mathematical Foundations of Programming Semantics (MFPS). [ bib | slides ]

Benjamin C. Pierce. Types and Programming Languages: The Next Generation, 2003. Invited tutorial at Logic in Computer Science (LICS). [ bib | slides ]

Benjamin C. Pierce. Advanced Module Systems: A Guide for the Perplexed, 2000. Invited tutorial at International Conference on Functional Programming (ICFP). [ bib | slides ]

Benjamin Pierce, Scott Dietzen, and Spiro Michaylov. Programming in Higher-order Typed Lambda-Calculi. Technical Report CMU-CS-89-111, Carnegie Mellon University, March 1989. [ bib | errata | tech report ]

Contracts

João Filipe Belo, Michael Greenberg, Atsushi Igarashi, and Benjamin C. Pierce. Polymorphic Contracts. In Gilles Barthe, editor, European Symposium on Programming (ESOP), Saarbrücken, Germany, volume 6602 of Lecture Notes in Computer Science, pages 18--37. Springer, 2011. [ bib ]

Michael Greenberg, Benjamin C. Pierce, and Stephanie Weirich. Contracts Made Manifest. In ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages (POPL), Madrid, Spain. ACM, January 2010. [ bib | short version ]

Benjamin C. Pierce. Types Considered Harmful, May 2008. Invited talk at Mathematical Foundations of Programming Semantics (MFPS). [ bib | slides ]

Modular Type Systems

Michael Y. Levin and Benjamin C. Pierce. TinkerType: A Language for Playing with Formal Systems. Journal of Functional Programming, 13(2), March 2003. A preliminary version appeared as an invited paper at the Logical Frameworks and Metalanguages Workshop (LFM), June 2000. [ bib | source code | full version | slides ]

Type Inference

Loris D'Antoni, Marco Gaboardi, Emilio Jesús Gallego Arias, Andreas Haeberlen, and Benjamin Pierce. Sensitivity analysis using type-based constraints. In Proceedings of the 1st annual workshop on Functional programming concepts in domain-specific languages, FPCDSL '13, pages 43--50, New York, NY, USA, 2013. ACM. [ bib | DOI | DOI | pdf ]

Haruo Hosoya and Benjamin C. Pierce. How Good is Local Type Inference? Technical Report MS-CIS-99-17, University of Pennsylvania, June 1999. [ bib | tech report ]

Benjamin C. Pierce and David N. Turner. Local Type Inference. In ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages (POPL), San Diego, California, 1998. Full version in ACM Transactions on Programming Languages and Systems (TOPLAS), 22(1), January 2000, pp. 1--44. [ bib | tech report | conference version | full version ]

Benjamin C. Pierce and David N. Turner. Local Type Argument Synthesis with Bounded Quantification. Technical Report 495, Computer Science Department, Indiana University, January 1997. [ bib | tech report ]

Object-Oriented Programming

Andrew J. Kennedy and Benjamin C. Pierce. On Decidability of Nominal Subtyping with Variance, September 2006. FOOL-WOOD '07. [ bib | short version ]

Atsushi Igarashi and Benjamin C. Pierce. On Inner Classes. Information and Computation, 177(1):56--89, August 2002. A special issue with papers from the 7th International Workshop on Foundations of Object-Oriented Languages (FOOL), informal proceedings. An earlier version appeared in \bgroup Proceedings of the 14th European Conference on Object-Oriented Programming (ECOOP), Springer LNCS 1850, pages 129--153. [ bib | tech report | conference version ]

Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. A Recipe for Raw Types. In Workshop on Foundations of Object-Oriented Languages (FOOL), 2001. [ bib | short version ]

Kim B. Bruce, Luca Cardelli, and Benjamin C. Pierce. Comparing Object Encodings. Information and Computation, 155(1/2):108--133, November 1999. Special issue of papers from Theoretical Aspects of Computer Software (TACS 1997). An earlier version appeared as an invited lecture in the Third International Workshop on Foundations of Object Oriented Languages (FOOL 3), July 1996. [ bib | .ps ]

Atsushi Igarashi, Benjamin Pierce, and Philip Wadler. Featherweight Java: A Minimal Core Calculus for Java and GJ. In ACM SIGPLAN Conference on Object Oriented Programming: Systems, Languages, and Applications (OOPSLA), October 1999. Full version in ACM Transactions on Programming Languages and Systems (TOPLAS), 23(3), May 2001. [ bib | conference version | full version ]

Atsushi Igarashi and Benjamin C. Pierce. Foundations for Virtual Types. In European Conference on Object-Oriented Programming (ECOOP), Lisbon, Portugal, June 1999. Also in informal proceedings of the Workshop on Foundations of Object-Oriented Languages (FOOL), January 1999. Full version in Information and Computation, 175(1): 34--49, May 2002. [ bib | .ps ]

Martin Hofmann and Benjamin C. Pierce. Type Destructors. In Didier Rémy, editor, Informal proceedings of the Fourth International Workshop on Foundations of Object-Oriented Languages (FOOL), January 1998. Full version in Information and Computation, 172(1)29--62 (2002). [ bib | conference version ]

Benjamin C. Pierce. Review of A Theory of Objects, by Abadi and Cardelli. The Computer Journal, 40(5):297--298, 1997. [ bib | .ps ]

Kim B. Bruce, Luca Cardelli, Giuseppe Castagna, the Hopkins Objects Group (Jonathan Eifrig, Scott Smith, Valery Trifonov), Gary T. Leavens, and Benjamin Pierce. On Binary Methods. Theory and Practice of Object Systems, 1(3):221--242, 1996. [ bib | .ps ]

Martin Hofmann and Benjamin Pierce. A Unifying Type-Theoretic Framework for Objects. Journal of Functional Programming, 5(4):593--635, October 1995. Previous versions appeared in the Symposium on Theoretical Aspects of Computer Science, 1994, (pages 251--262) and, under the title “An Abstract View of Objects and Subtyping (Preliminary Report),” as University of Edinburgh, LFCS technical report ECS-LFCS-92-226, 1992. [ bib | .ps ]

Martin Hofmann and Benjamin Pierce. Positive Subtyping. In ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages (POPL), San Francisco, California, pages 186--197, January 1995. Full version in Information and Computation, volume 126, number 1, April 1996. Also available as University of Edinburgh technical report ECS-LFCS-94-303, September 1994. [ bib | .ps ]

Benjamin C. Pierce and David N. Turner. Simple Type-Theoretic Foundations for Object-Oriented Programming. Journal of Functional Programming, 4(2):207--247, April 1994. Summary in ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages (POPL), Charleston, South Carolina, 1993. [ bib | conference version | pdf | .ps ]

Benjamin C. Pierce. Mutable Objects. Draft report; available electronically, June 1993. [ bib | .ps ]

Benjamin C. Pierce and David N. Turner. Statically Typed Friendly Functions via Partially Abstract Types. Technical Report ECS-LFCS-93-256, University of Edinburgh, LFCS, April 1993. Also available as INRIA-Rocquencourt Rapport de Recherche No. 1899. [ bib | .ps ]

Benjamin C. Pierce. A Model of Delegation Based on Existential Types. Available electronically, April 1993. [ bib | .ps ]

Subtyping

Andrew J. Kennedy and Benjamin C. Pierce. On Decidability of Nominal Subtyping with Variance, September 2006. FOOL-WOOD '07. [ bib | short version ]

Vladimir Gapeyev, Michael Levin, and Benjamin Pierce. Recursive Subtyping Revealed. Journal of Functional Programming, 12(6):511--548, 2003. Preliminary version in International Conference on Functional Programming (ICFP), 2000. Also appears as Chapter 21 of Types and Programming Languages by Benjamin C. Pierce (MIT Press, 2002). [ bib | conference version ]

Haruo Hosoya, Benjamin C. Pierce, and David N. Turner. Datatypes and Subtyping. Manuscript, 1998. [ bib | .ps ]

Benjamin C. Pierce. Bounded Quantification with Bottom. Technical Report 492, Computer Science Department, Indiana University, 1997. [ bib | tech report ]

Giuseppe Castagna and Benjamin Pierce. Corrigendum: Decidable Bounded Quantification. In Proceedings of the Twenty-Second ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages (POPL), Portland, Oregon. ACM, January 1995. [ bib | .ps ]

Benjamin C. Pierce. Bounded Quantification is Undecidable. Information and Computation, 112(1):131--165, July 1994. Also in C. A. Gunter and J. C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design, MIT Press, 1994. Summary in ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages (POPL), Albuquerque, New Mexico. [ bib | conference version ]

Benjamin C. Pierce and Martin Steffen. Higher-Order Subtyping. In IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET), 1994. Full version in Theoretical Computer Science, vol. 176, no. 1--2, pp. 235--282, 1997 (corrigendum in TCS vol. 184 (1997), p. 247). [ bib | tech report ]

Giuseppe Castagna and Benjamin Pierce. Decidable Bounded Quantification. In Proceedings of the Twenty-First ACM SIGPLAN--SIGACT Symposium on Principles of Programming Languages (POPL), Portland, Oregon. ACM, January 1994. [ bib | .ps ]

Giorgio Ghelli and Benjamin Pierce. Bounded Existentials and Minimal Typing, 1992. Circulated in manuscript form. Full version in Theoretical Computer Science, 193(1--2):75--96, February 1998. [ bib | .ps ]

Intersection and Union Types

Higher-Order Intersection Types and Multiple Inheritance, Adriana B. Compagnoni and Benjamin C. Pierce.

Intersection Types and Bounded Polymorphism, Benjamin C. Pierce. (Short version.)

Programming with Intersection Types and Bounded Polymorphism. Benjamin C. Pierce. (This file is identical to the printed thesis; it is set in the Palatino font, which is not available on all Postscript printers. If you have trouble printing it, try this instead. Or grab the PDF version.)

Programming With Intersection Types, Union Types, and Polymorphism, Benjamin C. Pierce.

Preliminary Investigation of a Calculus with Intersection and Union Types, Benjamin C. Pierce.

A Decision Procedure for the Subtype Relation on Intersection Types with Bounded Variables. Benjamin C. Pierce.

Extensible Records

A Record Calculus Based on Symmetric Concatenation, Robert W. Harper and Benjamin C. Pierce.

Dynamic Types

Dynamic Typing in a Statically Typed Language. Martin Abadi, Luca Cardelli, Benjamin Pierce, and Gordon Plotkin.

Dynamic Typing in Polymorphic Languages, Martin Abadi, Luca Cardelli, Benjamin Pierce, and Didier Remy.

Semantics

Faithful Ideal Models for Recursive Polymorphic Types, Martin Abadi, Benjamin Pierce, and Gordon Plotkin.

Grab Bag

Emacs Hacks

uuinsert.el, support for uu-encoding and uu-decoding of files and directories into text buffers.

reportmail.el, a mail-reporting package for emacs. Summarizes headers of incoming mail in the minibuffer and modeline.

spread.el: A simple emacs spreadsheet. (Guillaume Marceau has written a better version that you may want to try instead.)

Tex Hacks

Template for my latex slide style.

bcprules.sty. macros for typesetting inference rules.

Interactive Fiction

Woggles from Oz: Writing Interactive Fiction. Benjamin C. Pierce. (A short summary appeared in Leonardo: Journal of the International Society for the Arts, Sciences, and Technology, 1994.)

Old Stuff

Programming in Higher-Order Typed Lambda-Calculi, Benjamin Pierce, Scott Dietzen, and Spiro Michaylov. (Errata sheet)

Object-Oriented Programming in Typed Lambda-Calculus: Exercises and Solutions.

bctcs.errata for first printing of Basic Category Theory for Computer Scientists, Benjamin C. Pierce, MIT Press. (All the errors described here are corrected in the second printing.)

Standard-ML sources and binaries for "fmeet" and "fomega" typecheckers. Benjamin C. Pierce. (Probably hard to compile.)

Experimental typechecker for the type system described in my thesis -- a second-order lambda-calculus with bounded quantification and intersection types. Benjamin C. Pierce. (Probably hard to compile.)

Miscellaneous:

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 ]

Benjamin C. Pierce. Imagining the Reader, July 2022. Talk at Programming Languages Mentoring Workshop (PLMW). [ bib | slides ]

Keywords: Virtual conventions, Virtual conferences, Virtual meetings, Awareness, Social presence

Derek Dreyer and Benjamin C. Pierce. On being a PhD student of Robert Harper. Journal of Functional Programming, 32.32, 2022. [ bib ]

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 ]

Stephanie Weirich and Benjamin C. Pierce. ICFP 2020 Post-Conference Report. CoRR, abs/2104.01239, 2021. [ bib | arXiv | pdf ]

Benjamin C. Pierce, Michael Hicks, Crista Lopes, and Jens Palsberg. Conferences in an era of expensive carbon. Commun. ACM, 63(3):35--37, 2020. [ bib | DOI | DOI | pdf ]

Nicolas Koh, Yao Li, Yishuai Li, Li yao Xia, Lennart Beringer, Wolf Honore, William Mansky, Benjamin C. Pierce, and Steve Zdancewic. From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server. In 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, January 2019. [ bib | short version ]

Solomon Maina, Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, and Steve Zdancewic. Synthesizing Quotient Lenses. Proceedings of the ACM on Programming Languages (PACMPL ICFP), September 2018. [ bib | short version ]

Benjamin C. Pierce. In Memoriam Martin Hofmann, July 2018. The Apple Keynote version includes the music from the presentation, plus the full text in the presenter notes. [ bib | video | slides in Keynote format | slides ]

Richard Kim and Benjamin C. Pierce. Carbon Offsets: An Overview for Scientific Societies, June 2018. Version 1.2. [ bib | pdf ]

Benjamin C. Pierce. The Curse of Knowledge, January 2018. Talk at Programming Languages Mentoring Workshop (PLMW). [ bib ]

Jean Yang. People of Programming Languages: Interview with Benjamin Pierce, December 2017. [ bib | pdf ]

Benjamin C. Pierce. The Curse of Knowledge, January 2017. Talk at Programming Languages Mentoring Workshop (PLMW). [ bib | slides ]

Benjamin C. Pierce. creativity: sensitivity and surprise, October 2010. Keynote talk at SPLASH / Onward! [ bib | slides ]

Clowdr CIC. Midspace: An open-source platform for virtual academic conferences, 2020--2022. http://midspace.app. [ bib ]

Benjamin C. Pierce

Benjamin Pierce's Papers, Books, and Software

Recent Activities

Bibliography

Books

Specification, Verification, and Testing:

Security and Privacy:

Bidirectional Programming (Lenses):

Climate Change:

Synchronization

Native XML Processing in Statically Typed Languages

Xtatic

XDuce

Concurrent and Distributed Systems

Survey talks:

Mobile Agents

Pi-Calculus and Pict

Types

Surveys:

Contracts

Modular Type Systems

Type Inference

Object-Oriented Programming

Subtyping

Intersection and Union Types

Extensible Records

Dynamic Types

Semantics

Grab Bag

Emacs Hacks

Tex Hacks

Interactive Fiction

Old Stuff

Miscellaneous:

Benjamin Pierce's
Papers, Books, and Software