Skip to main content

Frank Pfenning

Department Head and Professor, School of Computer Science


Frank Pfenning

Research Areas

Privacy Protection

Cross Cutting Thrusts

Formal Methods, Software Security


Frank Pfenning joined the Department of Computer Science at Carnegie Mellon University as research faculty where he became Professor in 2002 and served as Director of Graduate Programs from 2004 to 2008. He has spent time as visiting scientist at the Max-Planck-Institute for Computer Science in Saarbrücken, as Alexander-von-Humboldt fellow at the Technical University Darmstadt, and as visiting professor at École Polytechnique and INRIA-Futurs. He has advised 19 completed Ph.D. theses and won the Herbert A. Simon Award for Teaching Excellence in the School of Computer Science in 2002. His research interests include programming languages, logic and type theory, logical frameworks, automated deduction, and computer security.


Mathematics and Computer Science at the Technical University Darmstadt
Carnegie Mellon University on a Fulbright scholarship where he obtained his Ph.D. in Mathematics in 1987.

Professional Background

He served as trustee, vice president, and president of CADE, Inc., the governing body of the International Conference on Automated Deduction, and on advisory boards for INRIA, the Max-Planck-Institute for Computer Science, and Seoul National University. He has chaired several conferences and program committees, including CADE and LICS, and is a member of the editorial boards for Theoretical Computer Science, Journal of Automated Reasoning, and the Journal of Symbolic Computation.


Research Projects

Secure Concurrent Distributed Programming

Cross Cutting Thrusts: Software Security | Formal Methods
Researcher: Frank Pfenning

Secure Distributed Logic Programming

Cross Cutting Thrusts: Formal Methods | Software Security
Researcher: Frank Pfenning

Compiling Epistemic Specifications to Secure Distributed Code

Cross Cutting Thrusts: Software Security | Formal Methods
Researcher: Frank Pfenning

Logical Reasoning About Obligations

Research Area: Privacy Protection
Cross Cutting Thrusts: Formal Methods
Researcher: Frank Pfenning

Privacy, Information Disclosure, & Authorization from a Logical Perspective

Researchers: Frank Pfenning, Lujo Bauer


"Logical approximation for program analysis". Robert J. Simmons and Frank Pfenning. Submitted to the Journal on Higher-Order and Symbolic Computation, March 2010.

"Possession as linear knowledge". Frank Pfenning. In B.Farwer, editor, Proceedings of the 3rd International Workshop on Logics, Agents, and Mobility (LAM 2010), Edinburgh, Scotland, July 2010. Abstract of invited talk. To appear.

" Refinement types for logical frameworks and their interpretation as proof irrelevance". William Lovas and Frank Pfenning. Logical Methods in Computer Science, May 2010. To appear.

"Session types as intuitionistic linear propositions". Luís Caires and Frank Pfenning. In P.Gastin and F.Laroussinie, editors, Proceedings of the 21st International Conference on Concurrency Theory (CONCUR 2010), Paris, France, August 2010. Springer LNCS. To appear.

"The practice and promise of substructural frameworks". Frank Pfenning. In K.Crary and M.Miculan, editors, Proceedings of 5th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2010), Edinburgh, Scotland, July 2010. Abstract of invited talk. To appear.