Frank Pfenning

Professor of Computer Science   Curriculum Vitæ    Frank Pfenning
Computer Science Department   Short Biography
fp@cs[]   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)
Session Types Message-Passing and Shared Memory Concurrency
C0 Specification and Verification in Introductory Computer Science
15-836 Substructural Logics
Fall'23, 12 units, TuTh 9:30-10:50, GHC 4215
(last instance Fall 2016)
15-317/657 Constructive Logic
Spring'23, 9 units, TuTh 8:00-9:20, TEP 1403

Recent Drafts, Talks, and Publications

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

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

Older Unpublished Drafts and Talks

Adjoint logic
Klaas Pruiksma, William 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.

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