Frank Pfenning
Curriculum Vitæ

Frank Pfenning   fp@cs[]
Computer Science Department
Department of Philosophy (courtesy)   +1 412 268-6343
Carnegie Mellon University    
Contents Academic Appointments | Visiting Positions | Education | Awards | Fellowships
Personal Information | Hobbies
University Service | Government Service | Advisory Boards | Summer Schools
Invited Talks | Tutorials | Summer Courses
Elsewhere Publications | Conference Committees | Professional Organizations | Journals
Teaching | Advising
Short Biography

Academic Appointments

2002-present Professor of Computer Science
2013-2018 Joseph F. Traub Professor and Head, Computer Science Department
2009-2010 Associate Dean for Graduate Education, School of Computer Science
2004-2008 Director of Graduate Programs, Computer Science Department
1999-2002 Associate Professor of Computer Science
1994-1999 Senior Research Computer Scientist
1988-1994 Research Computer Scientist
1986-1988 Research Associate

Visiting Positions

Jan-Aug 2019 Visiting Professor, Brown University
Jun-Jul 2006 Visiting Professor
LIX at École Polytechnique and INRIA-Futurs
Palaiseau, France
Jan-Jun 1996 Visiting Professor
Departments of Mathematics and Computer Science,
Technical University Darmstadt, Germany
Jun-Aug 1991 Visiting Scientist
Max-Planck Institute for Computer Science
Saarbrücken, Germany


1981-1986 Department of Mathematics, Carnegie Mellon University
Ph.D. January 1987
Thesis: Proof Transformations in Higher-Order Logic
Advisor: Professor Peter B. Andrews
1980-1981 Department of Mathematics, Carnegie Mellon University,
M.S. May 1981
1977-1980 Departments of Mathematics and Computer Science, Technical University Darmstadt
Vordiplom April 1979
1968-1977 Max-Planck-Gymnasium, Rüsselsheim, Abitur 1977
1964-1968 Albrecht-Dürer-Schule, Rüsselsheim


2021 PPDP 10 Year Most Influential Paper Award for Dependent Session Types via Intuitionistic Linear Type Theory, PPDP'11 (with Bernardo Toninho and Luís Caires).
2016 LICS Test of Time Award for A Linear Logical Framework, LICS'96 (with Iliano Cervesato).
Named Fellow of the ACM, for contributions to the logical foundations of automatic theorem proving and types for programming languages, 2015.
Herbert A. Simon Award for Teaching Excellence in Computer Science,
School of Computer Science, Carnegie Mellon University, May 2002.
Jugend Forscht,
State Champion Hessen, Mathematics/Computer Science, 1975.


Alexander-von-Humboldt Fellowship, Technical University Darmstadt, 1996
Research Fellowship, Carnegie Mellon University, 1981-1986
Fulbright Scholarship, Carnegie Mellon University, 1980-1981

Personal Information

Born in Rüsselsheim, Hessen, Germany
German citizen, U.S. permanent resident
Married to Nancy Pfenning, Lecturer Emeritus, Department of Statistics, University of Pittsburgh
Children Andreas and Marina
One brother (Robert) and one sister (Katja Funke)


Former chess (Schachverein Rüsselsheim)
mountain climbing (Alpenverein Rüsselsheim)
badminton (VfN Hattersheim, SV Disbu)
motocross (MSC Bauschheim)
soccer (SV 07 Raunheim, PA West Soccer, retd. 1996)
fencing (épée at Corsair Club Pittsburgh, retd. 2001)
Aborted experimental film appearance (Sharon Needles)
music video appearance ( Why do you think you are nuts?)
video channel
Current squash (PSQ; SCS Day 2008 snapshot a, snapshot b),
running, hiking, cooking, reading

University Service

CMU Faculty Review Committee, 2020-present.
CMU Academic Calendar Committee, 2020-present.
Cybersecurity and Privacy Education Committee, 2014-2016, 2019-present.
Speakers Club, 2001-present.
Computational Biology Head Search Committee (chair), 2019-2020.
SCS Council, 1991-1996, 2004-2010, 2013-2018.
Task Force on the CMU Experience, 2016-2017.
OSP/ORIC Advisory Committee, 2013-2015.
CSD Faculty Search Committee, 2012, 2013 (chair).
University Research Review Committee, 2007-2012.
Coordinator for SCS Dual Degree Programs with Portugal, 2007-2012.
Computer Science MS Degree Committee, 2010 (chair), 2011 (member).
Introductory CS Curriculum Committee, 2009-2010.
Associate Dean for Graduate Eduction, 2009-2010.
Academic Review Board, 2001-2008.
Departmental Review Committee (DRC), 1992-2001; chair 2004-2008.
CMU Graduate Student Service Award Committee, 2006.
CMU Barbara Lazarus Award Committee, 2005, 2007, 2008.
CSD Advisory Board Committee, 2005.
Hiring Committee, Associate Vice Provost of Graduate Education, 2005.
CSD Head Selection Committee, 2007.
Co-Chair, SCS Dean Search Committee, 2004.
Faculty Recruiting Committee, 1997, 2002, 2003.
Graduate Admissions Committee, 2002; Co-Chair 2003; 2005.
Reappointment and Promotions Committees, 1995-present.
Special Faculty Review Committee, 1995, 1999.
Lecturer Review Comittees, 1993-2000.
Undergraduate Curriculum Committee, Fall 2000.
Qualifier Review Committee (QRC), 1993-1995, 1998-1999.
POP Seminar Organization, 1991-1996.

Government Service

NASA Review Panel, 2003.
NSF Review Panels, 2002, 2003, 2009, 2010, 2014, 2016, 2019.

Advisory Boards

From Data Types to Session Types: A Basis for Concurrency and Distribution (ABCD), EPSRC Project
External Advisory Board, Membery, 2013-2018.
Department of Computer Science, ETH Zürich
Scientific Advisory Board,Chair November 2015.
School of Computer Science and Engineering, Seoul National University
External review committee, June 2007.
Max-Planck-Institut für Informatik, Saarbrücken, Germany.
International Ph.D. program evaluation committee, October 2004.
INRIA, Paris, France, October 2002.
Evaluation board for Theme 2A: sémantique et programmation.
Max-Planck-Institut für Informatik, Saarbrücken, Germany.
Scientific advisory board (Fachbeirat) Member, 2001-2006; Chair 2007-2012.

Summer Schools

Types, Logic, and Verification
Eugene, Oregon, July 22-August 3, 2013. Member of the scientific committee.
Software Security: Theory to Practice
Eugene, Oregon, June 17-25, 2004. Member of the scientific committee.
Foundations of Security
Eugene, Oregon, June 16-27, 2003. Member of the scientific committee.
Eugene, Oregon, June 24-July 5, 2002. Member of the scientific committee.
See also Summer Courses.


See Publications.

Invited Talks


A Rehabilitation of Message-Passing Concurrency
Papers We Love Conference (PWL'18),
St. Louis, Missouri, September 2018. [Animated Slides]
Substructural Proofs as Automata
14th Asian Symposium on Programming Languages and Systems (APLAS'14),
Hanoi, Vietnam, November 2016. [Paper]
On the Role of Proof Theory in Automated Deduction
25th International Conference on Automated Deduction (CADE-25),
Berlin, Germany, August 2015.
Polarized Substructural Session Types
18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'15),
London, England, April 2015. [Paper]
Subtyping and Intersection Types Revisited
12th International Conference on Functional Programming (ICFP'07),
Freiburg, Germany, October 2007. [Abstract]
On a Logical Foundation for Explicit Substitutions
Joint invited speaker, 18th International Conference on Rewriting Techniques and Applications (RTA'07) and
Typed Lambda Calculi and Applications (TLCA'07),
Paris, France, June 2007. [Abstract]
Substructural Operational Semantics and Linear Destination-Passing Style
Second Asian Symposium on Programming Languages and Systems (APLAS'04),
Taipei, Taiwan, November 2004. [Abstract]
Logical and Meta-Logical Frameworks
International Conference on Principles and Practice of Declarative Programming (PPDP'99),
Paris, France, September 1999.
Reasoning about Deductions in Linear Logic
15th International Conference on Automated Deduction (CADE-15),
Lindau, Germany, July 1998.
The Practice of Logical Frameworks
Colloquium on Trees in Algebra and Programming (CAAP'96),
Linköping, Sweden, April 1996.


How to Think About Types: Insights from a Personal Journey
Programming Languages Mentoring Workingship (PLMW'19)
Lisbon, Portugal, January 2019
A Shared Memory Semantics for Session Types
Workshop on Linearity and Trends in Linear Logic and Applications (Linearity/TLLA'18)
Oxford, England, July 2018. [Draft Paper]
Decomposing Modalities
10th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'15)
Berlin, Germany, August 2015.
Proof Theory and Its Role in Programming Language Research
Programming Languages Mentoring Workshop (PLMW'15)
Mumbai, India, January 2015.
Concurrent Programming in Linear Type Theory
Mathematical Structures of Computation,
Lyon, France, February 2014.
Towards Concurrent Type Theory
7th Workshop on Types in Language Design and Implementation (TLDI'12),
Philadelphia, Pennsylvania, January 2012.
Possession as Linear Knowledge
3rd International Workshopon Logics, Agents, and Mobility (LAM 2010),
Edinburgh, Scotland, July 2010. [Abstract]
The Practice and Promise of Substructural Frameworks
5th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2010),
Edinburgh, Scotland, July 2010. [Abstract]
Irrelevance as a Modality
Workshop on Intuitionistic Modal Logics and Applications (IMLA), Pittsburgh, Pennsylvania, June 2008.
Spurious Causal Dependency and Proof Irrelevance
Workshop on Logic Programming and Concurrency, Marseille, France, February 2006.
Towards a Type Theory of Contexts
Invited talk at Workshop on Mechanized Reasoning about Languages with Variable Binding (Merλin'05),
Tallinn, Estonia, September 2005.
Constructive Authorization Logics
Invited talk at the 4th Workshop on Foundations of Computer Security (FCS'05), Chicago, Illinois, July 2005.
Linear Logical Algorithms
Workshop on Programming Logics in Memory of Harald Ganzinger, Saarbrücken, Germany, June 2005.
Distributed System Security via Logical Frameworks
5th Workshop on Issues in the Theory of Security (WITS'05)
Long Beach, California, January 2005.
Tri-Directional Type Checking
Frank Pfenning, joint work with Jana Dunfield.
Workshop on Intersection Types and Related Systems (ITRS'02),
Copenhagen, Denmark, July 2002.
Three Applications of Strictness in the Efficient Implementation of Higher-Order Terms
Workshop on Implementations of Logic,
Réunion, France, November 2000.
Towards Modal Type Theory
Symposium on Constructivism in Non-Classical Logics and Computer Science, In Memoriam Pierangelo Miglioli,
Mantova, Italy, October 2000.
Reasoning About Staged Computation
Workshop on Semantics, Applications and Implementation of Program Generation (SAIG'00),
Montreal, Canada, September 2000.
On the Logical Foundations of Staged Computation
Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'00),
Boston, Massachusetts, January 2000. [Abstract]
A Judgmental Reconstruction of Modal Logics
Workshop on Intuitionistic Modal Logics and Applications,
Trento, Italy, July 1999.
Structural Cut Elimination
Workshop on Types for Proofs and Programs,
Turin, Italy, June 1995.
Refinement Types
Workshop on Logic, Domains and Programming Languages,
Darmstadt, Germany, May 1995.
Refinement Types for Logical Frameworks
Workshop on Types for Proofs and Programs,
Nijmegen, The Netherlands, May 1993.
Implementing the Meta-Theory of Deductive Systems
Third European Summer School on Language, Logic and Information,
Saarbrücken, Germany, August 1991.
Dependent Types in Logic Programming
Second Workshop on Extensions of Logic Programming, Stockholm, Sweden, January 1991.
Logical Frameworks and Logic Programming
Workshop on Logical Frameworks,
Sophia-Antipolis, France, May 1990.
Higher-Order Logic Programming
Meeting of the IFIP WG 2.3 on Programming Methodology,
Pittsburgh, Pennsylvania, August 1988.


Distributed System Security via Logical Frameworks
Computer Science Colloquium, McGill University, November 2005.
[Slides] (Powerpoint)
Modal Logic Revisited
Frank Pfenning.
Talk presented at The Scottfest in honor of Dana Scott on his 70th Birthday.
Pittsburgh, Pennsylvania, October 12, 2002. [Slides]
Verifying Program Invariants with Refinement Types
Princeton and Yale Colloquium Talks, February 2001. [Abstract] [Slides]
Max-Planck-Institut Saarbrücken, October 2001. [Abstract] [Slides]
Language Techniques for Provably Safe Mobile Code
Distinguished lecture, Computing and Information Sciences,
Kansas State University, October 2000. [Slides]


Message-Passing Concurrency and Substructural Logics
45th Symposium on Principles of Programming Languages (POPL'18),
Los Angeles, California, January 2018. [Live Code]
From Linear Logic to Session-Typed Concurrent Programming
42nd Symposium on Principles of Programming Languages (POPL'15),
Mumbai, India, January 2015.
Logical Frameworks
12th International Conference on Automated Deduction,
Nancy, France, June 1994.
Type Theory (with Peter Andrews)
11th International Conference on Automated Deduction,
Saratoga Springs, New York, June 1992.
Types in Logic Programming
9th International Conference on Logic Programming,
Jerusalem, Israel, June 1990.
Lambda Prolog (with Amy Felty, Elsa Gunter, and Dale Miller)
10th International Conference on Automated Deduction,
Kaiserslautern, Germany, July 1990.

Summer Courses

Session-Typed Concurrent Programming (5 lectures)
Summer School on Foundations of Probabilistic Programming and Security,
Eugene, Oregon, June 2019
Substructural Types Systems and Concurrent Programming (5 lectures)
Summer School on A Spectrum of Types,
Eugene, Oregon, June 2017
Basic Proof Theory (5 lectures)
Summer School on Types, Logic, Semantics, and Verification,
Eugene, Oregon, June 2015
Linear Logic and Session-Based Concurrency (5 lectures)
Summer School on Types, Logic, and Verification,
Eugene, Oregon, July 2013.
Proof Theory Foundations (4 lectures)
Summer School on Logic, Languages, Compilation, and Verification,
Eugene, Oregon, June 2010, June 2011, July 2012.
Logical and Meta-Logical Frameworks (4 lectures)
NATO Summer School on Proof and System Reliability,
Marktoberdorf, Germany, July 2001.
Reasoning about Programming Languages (5 lectures)
European Summer School on Language, Logic and Information,
Copenhagen, Denmark, August 1994.
Logical Frameworks and Logic Programming (5 hours)
Third European Summer School on Language, Logic and Information,
Saarbrücken, Germany, August 1991.

Conference Committees

See Conferences.

Professional Organizations

See Organizations.


See Courses.


See Students and Co-authors.

[ Home | Contact | Research | Publications | CV | Students ]
[ Projects | Courses | Conferences | Organizations | Journals ]
[ Logical Frameworks | Pittsburgh Squash Racquets Assocation ]

Frank Pfenning