Benjamin C. Pierce

Henry Salvatori Professor
Department of Computer and Information Science
University of Pennsylvania

Information

Coordinates, telephone numbers, schedule, and office hours
Capsule bio

Research

Recent publications and talks
All papers and software
Current/Recent Projects:
- Property-based testing
- VERSE: A unified environment for testing, SML-based, and Rocq-based development of verified C code
- Unison: A robust, portable file synchronizer
Books:
The Penn PL Club

Climate Change

Research:
- Carbon Connect, An NSF Expedition in Sustainable Computing
At Penn:
Conferences and air travel:
- Conferences in an Era of Expensive Carbon (CACM, 2020)
- Carbon Offsets: An Overview for Scientific Societies
- ACM Carbon Offsetting Policy (which I helped draft :-)
- Engaging with Climate Change: Possible Steps for SIGPLAN
- Virtual Conferences: A Guide to Best Practices
- SIGPLAN Climate Change page
- Midspace, a climate-focused, open-source virtual conference platform (currently dormant)

Teaching

Writing and Speaking with Style (public course materials)
Spring 2024: Foundations and Applications of Separation Logic (CIS 6700)
Older course materials: Writing and Speaking with Style (CIS810), Software Foundations (CIS500, many offerings), Advanced Topics in Programming Languages, CIS670: Verified Systems Software (Fall 2015), Advanced Topics in Programming Languages, CIS670: Advanced Martial Arts in Coq (Fall 2012), Programming Languages and Techniques I (CIS120 / 1200, many offerings), Advanced Programming (CIS552, 2008, 2014, etc.), Mathematical Foundations of Computer Science (CSE260, 2007), Proof Theory for Programming Languages (CIS700-009, 2005), Advanced Topics in Programming Languages (CIS670, 2011 and 2004), Distributed Data (CIS700, 2002), Global Computing (2001), Languages for Programming the Web (1997)

Professional Activities

Recent / Upcoming Meetings: PLDI 2025 (area chair), CSF 2025 (PC), OOPSLA 2024 (PC), FunArch 2024 (PC), Types 2024 (PC), OOPSLA 2023 (PC), POPL 2023 (PC), CoqPL 2023 (PC co-chair), Social Presence in Virtual Event Spaces (PC co-chair), CoqPL 2022 (PC co-chair), OOPSLA 2021 (ERC), ICFP 2020 (Virtualization chair), CPP 2020 (PC), OOPSLA 2019 (ERC), SecDev 2019 (PC), Types 2019 (PC), ICFP 2018 (ERC), OCAP 2017 (PC), CoqPL 2017 (PC), PLAS 2016 (PC), ICFP 2016 (ERC), SNAPL 2015 (PC), TPDP 2015 (PC), PLAS 2015 (PC), CSF 2014 (PC), PLAS 2014 (PC), POPL 2013 (PC), OPLSS 2012 (co-organizer), TLDI 2012 (PC chair), TLDI 2011 (PC), WMM 2010 (PC chair), OPLSS 2010 (lecturer), LFMTP 2010 (PC), PMMPS 2010 (PC), OOPSLA 2010 (PC), MFPS 2010 (PC), PLDI 2010 (ERC), FOSSACS 2010 (PC), POPL 2009 (PC chair), DSL 2009 (PC), WMM 2007 (SC), GTTSE 2007 (SC), LFMTP 2007 (PC), TFP 2007 (PC), DBPL 2007 (PC), ESOP 2007 (PC), TAP 2007 (PC), POPL 2007 (PC), PLAN-X 2006 (SC and PC), ICFP 2005 (PC chair), etc.
Editorial boards: Journal of Functional Programming (co-EIC, emeritus), Logical Methods in Computer Science (managing editor, emeritus), Mathematical Structures in Computer Science, Formal Aspects of Computing (FAC, emeritus), Electronic Proceedings in Theoretical Computer Science (EPTCS)
Groups: IFIP Working Group 2.8

Writing

Writing and Speaking with Style

Miscellaneous

Personal

Rogues Gallery