Frank Pfenning (original) (raw)
| search ~fp |
 |
| Home |
| Contact Information |
| Curriculum Vitæ |
| Research Interests |
| Publications |
| DBLP |
| Google Scholar Search |
| Google Scholar Profile |
| Students & Co-authors |
| Projects |
| Session Types |
| C0 |
| Courses |
| HOT Compilation 15-417/817 [Sp25] |
| Software Foundations 15-316 [Fa24] |
| Substructural Logics 15-836 [Fa23] |
| Constructive Logic 15-317 [Sp23] |
| Par. & Seq. Algorithms 15-210 [Fa22] |
| Bug Catching 15-414 [Sp22] |
| Types & Prog. Langs. 15-814 [Fa21] |
| Bug Catching 15-414 [Sp21] |
| Types & Prog. Langs. 15-814 [Fa20] |
| Functional Prog. 15-150 [Sp20] |
| Types & Prog. Langs. 15-814 [Fa19] |
| Types & Prog. Langs. 15-814 [Fa18] |
| Constructive Logic 15-317 [Fa17] |
| Substructural Logics 15-816 [Fa16] |
| Princs. Imp. Comp. 15-122 [Fa15] |
| Compiler Design 15-411 [Fa14] |
| Summer School |
| Oregon'22 |
| Oregon'19 |
| Oregon'17 |
| Oregon'15 |
| Oregon'13 |
| Conferences |
| TABLEAUX'23 PC |
| CSF'24 PC |
| ESOP'24 SC |
| Organizations |
| ACM SIGLOG |
| ACM SIGPLAN |
| Journals |
| JFP |
| http://www.cs.cmu.edu/~fp |
| 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-417/617/817 HOT Compilation Spring'25, 12 units, TuThu 12:30-2:50, PH A18C 15-316 Software Foundations of Security & Privacy Fall'24, 9 units, TuTh 2:00-3:20, PH 100 15-836 Substructural Logics Fall'23, 12 units, TuTh 9:30-10:50, GHC 4215 (last instance Fall 2016) 15-317/657 Constructive Logic Spring'23, 9 units, TuTh 8:00-9:20, TEP 1403 |
Recent Drafts, Talks, and Publications
See also Publications (as of July 29, 2023),DBLP,Google Scholar Profile
C. B. Aberlé, Chris Martens, and Frank Pfenning.
Under submission, February 2025.
Tutorial at POPL 2025
(introductory AI-generated podcast)
(live code)
Adjoint Natural Deduction (Extended Version)
Junyoung Jang, Sophia Roshal, Frank Pfenning, and Brigitte Pientka
Available as arXiv:2402.01428
Parametric Subtyping for Structural Parametric Polymorphism
Henry DeYoung, Andrei Mordido, Frank Pfenning, and Ankush Das
Symposium on Principles of Programming Languages (POPL 2024), 90:1-90:31 pp.
Distinguished paper award.
Artifact (in Standard ML)
So what's the difference between a session type and an ordinary type anyway?
30 Years of Session Types (ST30).
Cascais, Portugal, October 22, 2023.
Relating Message Passing and Shared Memory, Proof-Theoretically
Frank Pfenning and Klaas Pruiksma.
18th International Federated Conference on Distributed Computing Techniques (DisCoTec 2023).
Lisbon, Portugal, June 21, 2023.
Invited talk, Companion paper.
Data Layout from a Type-Theoretic Perspective
38th International Conference on Mathematical Foundations of Programming Semantics (MFPS'22),
Ithaca, New York and Paris, France, July 2022. [Incremental Slides]
Invited talk.
Modal Logics and Types: Looking Back and Looking Forward
Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'22), Philadelphia, Pennsylvania, January 2022.
Invited talk.
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
Klaas Pruiksma, Willow Chargin, Frank Pfenning, and Jason Reed.
Unpublished manuscript, April 2018.
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 ]