Frank Pfenning

President's Professor of Computer Science   Curriculum Vitæ    Frank Pfenning
Head, Department of Computer Science   Short Biography
fp@cs[.cmu.edu]   Picture
 
School of Computer Science   Office:   GHC 7019
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
MetaCLF Formal Reasoning about Languages for Distributed Computation
C0 Specification and Verification in Introductory Computer Science
Certified Interfaces Integrity and Security in Web-based Applications
more...
Courses
15-411/611 Compiler Design
Fall'13, 12 units, TuTh 1:30-2:50, HH B103

Recent Drafts, Talks, and Publications

Corecursion in Session-Typed Processes
Bernardo Toninho, Luís Caires, and Frank Pfenning.
Revised version to appear at TGC 2014.
A Linear Logic Programming Language for Concurrent Programming over Graph Structures
Flávio Cruz, Ricardo Rocha, Seth Goldstein, and Frank Pfenning.
Revised version to appear at ICLP 2014.
Book Review: Programming with Higher-Order Logic
by Dale Miller and Gopalan Nadathur, Cambridge University Press, 2012.
Theory and Practice of Logic Programming 14(2), pp. 265-267.
© Cambridge University Press. Definitive version
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.
Logic-Based Domain-Aware Session Types
Luís Caires, Jorge A. Pérez, Frank Pfenning, and Bernardo Toninho.
Submitted.
Linear Logical Relations and Observational Equivalences for Session-Based Concurrency
Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho.
Submitted.
Higher-Order Processes, Functions, and Sessions: A Monadic Integration
Bernardo Toninho, Luís Caires, and Frank Pfenning.
European Symposium on Programming (ESOP), pp. 350-369, March 2013.
Behavioral Polymorphism and Parametricity in Session-Based Communication
Luís Caires, Jorge A. Pérez, Frank Pfenning, and Bernardo Toninho.
European Symposium on Programmin (ESOP), pp. 330-349, March 2013.
Complete list of publications

Older Unpublished Drafts and Talks

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