|
Frank Pfenning
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)
|
|
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
-
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
]
http://www.cs.cmu.edu/~fp
|