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, publications, talks, students & co-authors)
Session Types Message-Passing and Shared Memory Concurrency
C0 Specification and Verification in Introductory Computer Science
15-317/657 Constructive Logic
Spring'23, 9 units, TuTh 8:00-9:20, TEP 1403
15-210 Parallel and Sequential Data Structures and Algorithms
Fall'22, 12 units, MoWe(Fr) 10:10-11:30, GHC 4401
15-414/614 Bug Catching: Automated Program Verification
Spring'22, 9 units, TuTh 11:50-1:10, IPE except weeks 1 & 2
15-814 Types and Programming Languages
Fall'21, 12 units, TuTh 10:10-11:30, GHC 4301 (IPE)

Recent Drafts, Talks, and Publications

See also Publications (as of Jan 3, 2021), DBLP, Google Scholar Profile

Modal Logics and Types: Looking Back and Looking Forward
Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM).
Invited Talk. January 17, 2022.
Subtyping on Nested Polymorphic Session Types
Ankush Das, Henry DeYoung, Andrea Mordido, and Frank Pfenning.
Technical Report, avilable as arXiv:2013.15193.
March 2021.
Manifestly Phased Communication via Shared Session Types
Chuta Sano, Stephanie Balzer, and Frank Pfenning.
Technical Report, available as arXiv:2101.06249.
January 2021.
Rast: A Language for Resource-Aware Session Types
Ankush Das and Frank Pfenning.
Submitted, December 2020.
Rast is available at
15-814 Types and Programming Languages
Frank Pfenning.
Combined course notes for 15-814, December 2020.
An implementation of the Lambda language is available at

Older Unpublished Drafts and Talks

Teaching Imperative Programming with Contracts at the Freshmen Level [Experience Report]
Frank Pfenning, Thomas J. Cortina, and William Lovas.
Unpublished manuscript, September 2011.
Updated version:
An Approach to Teaching to Write Safe and Correct Imperative Programs --- Even in C,
Iliano Cervesato, Thomas J. Cortina, Frank Pfenning, and Saquib Razak,
January 2019.
The Focused Constraint Inverse Method for Intuitionistic Modal Logics
Sean McLaughlin and Frank Pfenning.
Draft manuscript, January 2010.

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