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

Recent Drafts, Talks, and Publications

See also Publications (as of November 12, 2025), DBLP, Google Scholar Profile

Talk On the Normative Power of Logical Frameworks in memory of Gilles Dowek, July 2026

Papers relating to the lectures on Proof-Theoretic Compilation at the 6th Summer School on Foundations of Programming and Software Systems (FoPSS 2026)

• Snax compiler
• Joanna Boyland and Frank Pfenning.
  Proof-Theoretic Adjoint Compilation.
  Draft manuscript, January 2026. [pdf]
• Junyoung Jang, Sophia Roshal, Frank Pfenning, and Brigitte Pientka.
  Adjoint natural deduction.
  In Jakob Rehof, editor, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024), pages 15:1–15:23, Tallinn, Estonia, July 2024. LIPIcs 299. Extended version available as https://arxiv.org/abs/2402.01428. [ bib ]
• Frank Pfenning and Klaas Pruiksma.
  Relating message passing and shared memory, proof-theoretically.
  In S. Jongmans and A. Lopes, editors, 25th International Conference on Coordination Models and Languages (COORDINATION 2023), pages 3–27, Lisbon, Portugal, June 2023. Springer LNCS 13908. Notes to an invited talk. [ bib | pdf ]
• Henry DeYoung and Frank Pfenning.
  Data layout from a type-theoretic perspective.
  In 38th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2022). Electronic Notes in Theoretical Informatics and Computer Science 1, 2022. Invited paper. Extended version available at https://arxiv.org/abs/2212.06321v3.pdf. [ bib | http | pdf ]
• Henry DeYoung, Frank Pfenning, and Klaas Pruiksma.
  Semi-axiomatic sequent calculus.
  In Z. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), pages 29:1–29:22, Paris, France, June 2020. LIPIcs 167. [ bib | pdf ]

Ordered Adjoint Logic

Sophia Roshal and Frank Pfenning.
IJCAR 2026, to appear.

Security Reasoning via Substructural Dependency Tracking

Hemant Gouni, Frank Pfenning, and Jonathan Aldrich.
POPL 2026, pp. 777-805. (Open Access)

Structural Information Flow: A Fresh Look at Types for Non-Interference

Hemant Gouni, Frank Pfenning, and Jonathan Aldrich.
OOPSLA 2025, pp. 3954-3980. (Open Access)

Substructural Parametricity

C. B. Aberlé, Karl Crary, Chris Martens, and Frank Pfenning.
FSCD 2025. (Open Access)

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, Andreia 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.

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.

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

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