Frank Pfenning

Professor of Computer Science	Curriculum Vitæ
Associate Dean for Graduate Education	Short Biography
School of Computer Science
fp@cs[.cmu.edu]	Picture

Department of Computer Science	Office:	GHC 9101
Carnegie Mellon University	Phone:	+1 412 268-6343
Pittsburgh, PA 15213-3891, U.S.A.	Fax:	+1 412 268-3608

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

Certified Interfaces	for Integrity and Security in Web-based Applications
Prospero	Integrating Types and Specifications
Manifest Security	Logics and Languages for Manifestly Secure Systems
Twelf	Logical and Meta-Logical Frameworks
more...

Courses

15-122 Principles of Imperative Computation
Fall'10, 10 units, TuTh 9:00-10:20, GHC 4401

15-816 Modal Logic
Spring'10, 12 units, TuTh 1:30-2:50, GHC 4102

15-317 Constructive Logic
Fall'09, 9 units, TuTh 12:00-1:20, GHC 4102

15-411 Compiler Design
Fall'09, 12 units, TuTh 1:30-2:50, GHC 4102

Conferences

LPAR-17	(PC Member)	Yogyakarta, Indonesia, October 10-15, 2010 Abstracts due June 1, 2010 Papers due June 8, 2010

Organizations

LICS	OC Member, 2008-present	(Logic in Computer Science)
CADE	Trustee, 1998-2004	(Conference on Automated Deduction)
GPCE	SC Member, 2003-2007	(Generative Programming and Component Engineering)
PPDP	SC Member, 2000-2004	(Principles and Practice of Declarative Programming)
MPII	Advisory Board, 2001-present	(Max-Planck-Institut für Informatik, Saarbrücken)

Journals

TCS	Editor, 2005-2009	(Theoretical Computer Science)
JAR	Editor, 2001-2009	(Journal of Automated Reasoning)
JSC	Editor, 2000-2009	(Journal of Symbolic Computation)

Home Pages

CMU Squash Ladder

Recent Drafts, Talks, and Publications

Possession as Linear Knowledge: 3rd International Workshopon Logics, Agents, and Mobility (LAM 2010),
Edinburgh, Scotland, July 2010. [Abstract]
The Practice and Promise of Substructural Frameworks: 5th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2010),
Edinburgh, Scotland, July 2010. [Abstract]
Session Types as Intuitionistic Linear Propositions: Luís Caires and Frank Pfenning.
April 2010. Revised version to appear at CONCUR 2010, Paris, France, August 2010.
Refinement Types for Logical Frameworks and Their Interpretation as Proof Irrelevance: William Lovas and Frank Pfenning.
Logical Methods in Computer Science, To appear.
Version from May 2010.
Logical Approximation for Program Analysis: Robert J. Simmons and Frank Pfenning.
Submitted, March 2010.
A Proof-Carrying File System: Deepag Garg and Frank Pfenning.
Symposium on Security and Privacy (Oakland), May 2010.
Expanded Technical Report CMU-CS-09-123, Implementation
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.
Reasoning about the Consequences of Authorization Policies in a Linear Epistemic Logic: Henry DeYoung and Frank Pfenning.
Workshop on Foundations of Computer Security (FCS), Los Angeles, California,
Informal Proceedings, pp. 9-23, August 2009. [Slides by Henry DeYoung]
A Logical Representation of Common Rules for Controlling Access to Classified Information: Deepak Garg, Frank Pfenning, Denis Serenyi, and Brian Witten.
Technical Report CMU-CS-09-139, June 2009.
Substructural Operational Semantics as Ordered Logic Programming: Frank Pfenning and Robert J. Simmons.
LICS'09, Los Angeles, California, pp. 101-110, August 2009.
Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method: Sean McLaughlin and Frank Pfenning.
CADE-22, Montreal, Canada, pp. 230-244, August 2009.
On Linear Inference: Frank Pfenning.
Short expository note, February 2008.
Linear Logical Approximations: Robert J. Simmons and Frank Pfenning.
Proceedings of the Workshop on Partial Evaluation and Program Manipulation (PEPM'09), pp.9-20, Savannah, Georgia, USA, January 2009.
Church and Curry: Combining Intrinsic and Extrinsic Typing: Frank Pfenning.
Festschrift in Honor of Peter B. Andrews on His 70th Birthday.
Studies in Logic and the Foundation of Mathematics, IFCoLog, 2008.

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