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, talks, and publications publications, students & co-authors)

Projects

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
more...

Courses

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

A Shared Memory Semantics for Session Types: Invited talks, Linearity/TLLA 2018, Oxford, UK, July 2018.
Reporting on joint work with Klaas Pruiksma.
Related draft paper: Asynchronous Multistructural 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.
Work Analysis with Resource-Aware Session Types: Ankush Das, Jan Hoffmann, and Frank Pfenning.
LICS 2018, to appear.
Session-Typed Concurrent Contracts: Hannah Gommerstadt, Limin Jia, and Frank Pfenning.
European Symposium on Programming (ESOP'18), pp. 771-798, April 2018.
A Universal Session Type for Untyped Asynchronous Communication: Stephanie Balzer, Frank Pfenning, and Bernardo Toninho.
Draft of April 2018.
CONCUR 2018, to appear.
Adjoint Logic: Klaas Pruiksma, William Chargin, Frank Pfenning, and Jason Reed.
Under submission, April 2018.
Parallel Complexity Analysis with Temporal Session Types: Ankush Das, Jan Hoffmann, and Frank Pfenning.
Draft of March 2018.
ICFP 2018, to appear.
Adjoint Logic and Its Concurrent Operational Interpretation: Klaas Pruiksma, William Chargin, Frank Pfenning, and Jason Reed.
Draft manuscript, January 2018.
Message-Passing Concurrency and Substructural Logics: Slides for a POPL 2018 tutorial, January 2018.
Live-coded examples (popl18-live.zip)
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.
Slides
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.
Slides
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: https://github.com/ISANobody/sill
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.
Submitted.
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.
[Abstract]
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.

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