Frank Pfenning
Curriculum Vitæ

Academic Appointments

Visiting Positions

Education

Awards

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.

Fellowships

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)

Hobbies

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

>Mathematics and Computer Science Department, Wesleyan University

External Advisory Board, Member, 2021

From Data Types to Session Types: A Basis for Concurrency and Distribution (ABCD), EPSRC Project

External Advisory Board, Member, 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.

Proofs-as-Programs

Eugene, Oregon, June 24-July 5, 2002. Member of the scientific committee.

See also Summer Courses.

Publications

See Publications.

Invited Talks

Conferences

Relating Message Passing and Shared Memory, Proof-Theoretically

Conference on Coordination Models and Languages (COORDINATION'23),
Lisbon, Portugal, June 2023.

Data Layout from a Type-Theoretic Perspective

38th International Conference on Mathematical Foundations of Programming Semantics (MFPS'22),
Ithaca, New York and Paris, France, July 2022. [Incremental Slides]

Modal Logics and Types: Looking Back and Looking Forward

Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'22), Philadelphia, Pennsylvania, January 2022.

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.

Workshops

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

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.

Universities

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]

Tutorials

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

Introduction to Proof Theory (5 lectures)

Summer School on Types, Semantics, and Program Reasoning,
Eugene, Oregon, June 2022

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.

Teaching

See Courses.

Advising

See Students and Co-authors.

[ Home | Contact | Research | Publications | CV | Students ]
[ Projects | Courses | Conferences | Organizations | Journals ]

Frank Pfenning