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

Projects

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

Courses

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 https://bitbucket.org/fpfenning/rast/src/master/rast/
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
http://www.cs.cmu.edu/~fp/courses/15814-f20/software.html

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.

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