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

Session Types	Message-Passing Concurrency
C0	Specification and Verification in Introductory Computer Science

Courses

15-150 Functional Programming
Spring'20, 10 units, Lec 2, TuTh 3:00-4:20, WeH 7500

15-814 Types and Programming Languages
Fall'19, 12 units, TuTh 10:30-11:50, GHC 4215

Recent Drafts, Talks, and Publications

Rast: Resource-Award Session Types with Arithmetic Refinements (System Description): Ankush Das and Frank Pfenning.
Submitted, February 2020.
Rast is available at https://bitbucket.org/fpfenning/rast/src/master/rast/
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 (popl18-live.zip)
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: https://github.com/ISANobody/sill
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.
[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