Frank Pfenning

Joseph F. Traub Professor of Computer Science   Curriculum Vitæ    Frank Pfenning
Head, Computer Science Department   Short Biography
fp@cs[]   Picture
School of Computer Science   Office:   GHC 7019
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)
MetaCLF Formal Reasoning about Languages for Distributed Computation
C0 Specification and Verification in Introductory Computer Science
Certified Interfaces Integrity and Security in Web-based Applications
15-317/15-657 Constructive Logic
Fall'17, 9 units, TuTh 1:30pm-2:50pm, GHC 4307
15-816 Substructural Logics
Fall'16, 12 units, TuTh 1:30pm-2:50pm, GHC 4301

Recent Drafts, Talks, and Publications

Adjoint Logic and Its Concurrent Operational Interpretation
Klaas Pruiksma, William Chargin, Frank Pfenning, and Jason Reed.
Under submission, January 2018.
Work Analysis with Resource-Aware Session Types
Ankush Das, Jan Hoffmann, and Frank Pfenning.
Under submission, January 2018.
Message-Passing Concurrency and Substructural Logics
Slides for a POPL 2018 tutorial, January 2018.
Live-coded examples (
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.
Manifest Sharing with Session Types
Stephanie Balzer and Frank Pfenning.
ICFP, September 2017, to appear.
Technical Report CMU-CS-17-106R (revised extended version)
Substructural Proofs as Automata
Henry DeYoung and Frank Pfenning.
Notes for an invited talk at APLAS 2016, Hanoi, Vietnam, November 2016.
Design and Implementation of Concurrent C0
Max Willsey, Rokhini Prabhu, and Frank Pfenning.
Revised version to appear at Linearity 2016, Porto, Portugal.
Non-Blocking Concurrent Imperative Programming with Session Types
Miguel Silva, Mário Florido, and Frank Pfenning.
Revised version to appear at Linearity 2016, Porto, Portugal.
An Isomorphism Between Substructural Proofs and Deterministic Finite Automata
Henry DeYoung and Frank Pfenning.
Submitted, April 2016.
Intersections and Unions of Session Types
Coşku Acay and Frank Pfenning.
Revised version to appear at ITRS 2016, Porto, Portugal.
Monitors and Blame Assignment for Higher-Order Session Types
Limin Jia, Hannah Gommerstadt, and Frank Pfenning.
POPL 2016, St. Petersburg, Florida, January 2016.
Slides (by Hannah Gommerstadt)
Objects as Session-Typed Processes
Stephanie Balzer and Frank Pfenning.
Agere!, Pittsburgh, Pennsylvania, October 2015.
Slides (by Stephanie Balzer)
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.
Polarized Substructural Session Types
Frank Pfenning and Dennis Griffith.
18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2015),
London, UK, April 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:
Corecursion and Non-Divergence in Session-Typed Processes
Bernardo Toninho, Luís Caires, and Frank Pfenning.
9th International Symposium on Trustworthy Global Computing (TGC 2014)
Rome, Italy, September 2014. To appear.
A Linear Logic Programming Language for Concurrent Programming over Graph Structures
Flávio Cruz, Ricardo Rocha, Seth Goldstein, and Frank Pfenning.
30th International Conference on Logic Programming (ICLP 2014)
Vienna, Austria, July 2014. To appear. Best paper award.
Book Review: Programming with Higher-Order Logic
by Dale Miller and Gopalan Nadathur, Cambridge University Press, 2012.
Theory and Practice of Logic Programming 14(2), pp. 265-267.
© Cambridge University Press. Definitive version
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.
Logic-Based Domain-Aware Session Types
Luís Caires, Jorge A. Pérez, Frank Pfenning, and Bernardo Toninho.
Linear Logical Relations and Observational Equivalences for Session-Based Concurrency
Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho.
A revised version has been accepted to Information & Computation.
Higher-Order Processes, Functions, and Sessions: A Monadic Integration
Bernardo Toninho, Luís Caires, and Frank Pfenning.
European Symposium on Programming (ESOP), pp. 350-369, March 2013.
Behavioral Polymorphism and Parametricity in Session-Based Communication
Luís Caires, Jorge A. Pérez, Frank Pfenning, and Bernardo Toninho.
European Symposium on Programmin (ESOP), pp. 330-349, March 2013.
Complete list of publications

Older Unpublished Drafts and Talks

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 ]