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, talks, and publications publications, students & co-authors)
Session Types Message-Passing and Shared Memory Concurrency
C0 Specification and Verification in Introductory Computer Science
15-814 Types and Programming Languages
Fall'20, 12 units, TuTh 9:50-11:10, REMOTE
15-150 Functional Programming
Spring'20, 10 units, Lec 2, TuTh 3:00-4:20, WeH 7500

Recent Drafts, Talks, and Publications

Rast: Resource-Aware Session Types with Arithmetic Refinements (System Description)
Ankush Das and Frank Pfenning.
Submitted, February 2020.
Rast is available at
Semi-Axiomatic Sequent Calculus
Henry DeYoung, Frank Pfenning, and Klaas Pruiksma.
Submitted, February 2020.
Circular Proofs in First-Order Linear Logic with Least and Greatest Fixed Points
Farzaneh Derakhshan and Frank Pfenning.
Submitted, January 2020.
Session Types with Arithmetic Refinements and Their Application to Work Analysis
Ankush Das and Frank Pfenning.
Submitted, January 2020.
Available as arXiv:2001.04439 [cs.PL].
Back to Futures
Klaas Pruiksma and Frank Pfenning.
Draft manuscript, October 2019.
Available as arXiv:2002.04607 [cs.PL].
Circular Proofs as Session-Typed Processes: A Local Validity Condition
Farzaneh Derakhshan and Frank Pfenning.
Available as arXiv:1908.01909 [cs.LO].
Domain-Aware Session Types
Luis Caires, Jorge A. Perez, Frank Pfenning, and Bernardo Toninho.
CONCUR 2019, Amsterdam, The Netherlands, August 2019.
A Message-Passing Interpretation of Adjoint Logic
Klaas Pruiksma and Frank Pfenning.
PLACES 2019, April 2019.
Manifest Deadlock-Freedom for Shared Session Types
Stephanie Balzer, Bernardo Toninho, and Frank Pfenning.
ESOP 2019, Prague, Czech Republic.
Resource-Aware Session Types for Digital Contracts
Ankush Das, Stephanie Balzer, Jan Hoffmann, and Frank Pfenning.
Submitted, March 2019.
How to think about types: Insights from a personal journey
Talk at the Programming Languages Mentoring Workshop (PLMW)
Lisbon, Portugal, January 2019.
A Shared-Memory Semantics for Mixed Linear and Non-Linear Session Types
Klaas Pruiksma and Frank Pfenning.
Draft manuscript, November 2018.
A Rehabilitation of Message-Passing Concurrency
Talk, Papers We Love Conf, September 2018.
Dedicated to Kohei Honda, Types for Dyadic Interaction, CONCUR 1993.
(incremental slides)
A Shared Memory Semantics for Session Types
Invited talk, Linearity/TLLA 2018, Oxford, UK, July 2018.
Reporting on joint work with Klaas Pruiksma.
Related draft paper: A Shared-Memory Semantics for Mixed Linear and Non-Linear Session Types
Ergometric and Temporal Session Types
Invited talk, MFPS 2018, Halifax, Nova Scotia, June 2018.
Reporting on joint work with Ankush Das and Jan Hoffmann.
Message-Passing Concurrency and Substructural Logics
Slides for a POPL 2018 tutorial, January 2018.
Live-coded examples (
Complete list of publications

Older Unpublished Drafts and Talks

Adjoint Logic and Its Concurrent Semantics
Slides for a talk at the ABCD Project Meeting, Edinburgh, Scotland, December 2017.
Joint work with Klaas Pruiksma and William Chargin.
A paper is in preparation.
An Isomorphism Between Substructural Proofs and Deterministic Finite Automata
Henry DeYoung and Frank Pfenning.
Submitted, April 2016.
On the Role of Proof Theory in Automated Deduction
25th International Conference on Automated Deduction (CADE-25).
Berlin, Germany, August 2015.
Invited talk at the special session on the past, present, and future of automated deduction.
Update: As of Aug 6, 2015, the admissibility of cut and identity expansion for focused polarized adjoint logic has been checked.
Decomposing Modalities
10th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2015).
Berlin, Germany, August 2015.
Invited talk.
Proof Theory and Its Role in Programming Language Research
Programming Languages Mentoring Workshop (PLMW 2015),
Mumbai, India, January 2015
From Linear Logic to Session-Typed Concurrent Programming
Tutorial at POPL 2015, Mumbai, India, January 2015
Joint work with Luís Caires, Bernardo Toninho, and Dennis Griffith
Live code: primes.sill queue-data.sill
SILL implementation in OCaml:
Concurrent Programming in Linear Type Theory
Mathematical Structures of Computation
Lyon, February 2014.
Earlier version presented at the ABCD Project Meeting.
Imperial College, London, January 2014.
Church and Curry: Combining Intrinsic and Extrinsic Typing
Talk dedicated to Peter Andrews on the occasion of his retirement. April 5, 2012.
A related paper paper appeared in:
Reasoning in Simple Type Theory, Festschrift in Honor of Peter B. Andrews on His 70th Birthday, pp. 303-338, College Publications, London, 2008.
Teaching Imperative Programming with Contracts at the Freshmen Level [Experience Report]
Frank Pfenning, Thomas J. Cortina, and William Lovas.
Unpublished manuscript, September 2011.
Possession as Linear Knowledge
3rd International Workshopon Logics, Agents, and Mobility (LAM 2010),
Edinburgh, Scotland, July 2010. Invited Talk.
The Focused Constraint Inverse Method for Intuitionistic Modal Logics
Sean McLaughlin and Frank Pfenning.
Draft manuscript, January 2010.
Focus-Preserving Embeddings of Substructural Logics in Intuitionistic Logic
Jason Reed and Frank Pfenning.
Draft manuscript, January 2010.

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