Frank Pfenning

Professor of Computer Science	Curriculum Vitæ
Computer Science Department	Short Biography
fp@cs[.cmu.edu]	Picture

School of Computer Science	Office:	GHC 6017
Carnegie Mellon University	Phone:	+1 412 268-6343
Pittsburgh, PA 15213-3891, U.S.A.	Fax:	+1 412 268-5577

Research Interests

Programming Languages, Logic and Type Theory,
Logical Frameworks, Automated Deduction, Trustworthy Computing
(see also recent drafts, publications, talks, students & co-authors)

Projects

Session Types	Message-Passing and Shared Memory Concurrency
C0	Specification and Verification in Introductory Computer Science

Courses

15-814 Types and Programming Languages
Fall'25, 12 units, TuTh 12:30-1:50, WeH 8427

15-417/617/817 HOT Compilation
Spring'25, 12 units, TuTh 12:30-1:50, PH A18C

Recent Drafts, Talks, and Publications

See also Publications (as of July 29, 2023), DBLP, Google Scholar Profile

Substructural Parametriciy: C. B. Aberlé, Chris Martens, and Frank Pfenning.
Under submission, February 2025.
Substructural Type Systems: Tutorial at POPL 2025
(introductory AI-generated podcast)
(live code)
Adjoint Natural Deduction (Extended Version): Junyoung Jang, Sophia Roshal, Frank Pfenning, and Brigitte Pientka
Available as arXiv:2402.01428
Parametric Subtyping for Structural Parametric Polymorphism: Henry DeYoung, Andrei Mordido, Frank Pfenning, and Ankush Das
Symposium on Principles of Programming Languages (POPL 2024), 90:1-90:31 pp.
Distinguished paper award.
Artifact (in Standard ML)
So what's the difference between a session type and an ordinary type anyway?: 30 Years of Session Types (ST30).
Cascais, Portugal, October 22, 2023.
Relating Message Passing and Shared Memory, Proof-Theoretically: Frank Pfenning and Klaas Pruiksma.
18th International Federated Conference on Distributed Computing Techniques (DisCoTec 2023).
Lisbon, Portugal, June 21, 2023.
Invited talk, Companion paper.
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]
Invited talk.
Modal Logics and Types: Looking Back and Looking Forward: Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'22), Philadelphia, Pennsylvania, January 2022.
Invited talk.
15-814 Types and Programming Languages: Frank Pfenning.
Combined course notes for 15-814, December 2020.
An implementation of the Lambda language is available at
http://www.cs.cmu.edu/~fp/courses/15814-f20/software.html

Older Unpublished Drafts and Talks

Adjoint logic: Klaas Pruiksma, Willow Chargin, Frank Pfenning, and Jason Reed.
Unpublished manuscript, April 2018.
Teaching Imperative Programming with Contracts at the Freshmen Level [Experience Report]: Frank Pfenning, Thomas J. Cortina, and William Lovas.
Unpublished manuscript, September 2011.
Updated version:
An Approach to Teaching to Write Safe and Correct Imperative Programs --- Even in C,
Iliano Cervesato, Thomas J. Cortina, Frank Pfenning, and Saquib Razak,
January 2019.
The Focused Constraint Inverse Method for Intuitionistic Modal Logics: Sean McLaughlin and Frank Pfenning.
Draft manuscript, January 2010.

http://www.cs.cmu.edu/~fp