Frank Pfenning

Professor of Computer Science   Curriculum Vitæ    Frank Pfenning
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-814 Types and Programming Languages
Fall'18, 12 units, TuTh 10:30-11:50, GHC 4307

Recent Drafts, Talks, and Publications

A Message-Passing Interpretation of Adjoint Logic
Klaas Pruiksma and Frank Pfenning.
Submitted, January 2019.
How to think about types: Insights from a personal journey
Talk at the Programming Languages Mentoring Workshop (PLMW)
Lisbon, Portugal, January 2019.
Resource-Aware Session Types for Digital Contracts
Ankush Das, Stephanie Balzer, Jan Hoffmann, and Frank Pfenning.
Submitted, November 2018.
Manifest Deadlock-Freedom for Shared Session Types
Stephanie Balzer, Bernardo Toninho, and Frank Pfenning.
Revised version to appear at ESOP 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.

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

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