Frank Pfenning

President's Professor of Computer Science	Curriculum Vitæ
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

Programming Languages, Logic and Type Theory,
Logical Frameworks, Automated Deduction, Trustworthy Computing
(see also recent drafts, talks, and publications publications, students & co-authors)

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...

15-411/611 Compiler Design
Fall'13, 12 units, TuTh 1:30-2:50, HH B103

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.
A Linear Logic Programming Language for Concurrent Programming over Graph Structures: Flávio Cruz, Ricardo Rocha, Seth Goldstein, and Frank Pfenning.
Submitted.
Logic-Based Domain-Aware Session Types: Luís Caires, Jorge A. Pérez, Frank Pfenning, and Bernardo Toninho.
Submitted.
Corecursion in Session-Typed Processes: Bernardo Toninho, Luís Caires, and Frank Pfenning.
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

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.