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
Spring'11, 10 units, TuTh 9:00-10:20, GHC 4401

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

Conferences

CADE-23	(PC Member)	Wroclaw, Poland, July 31-August 5, 2011 Abstracts due Feb 1, 2011 Papers due Feb 7, 2011
ICFP 2011	(PC Member)	Tokyo, Japan, September 19-21, 2011 Abstracts due Mar 17, 2011 Papers due Mar 24, 2011

Organizations

LICS	OC Member, 2008-2010	(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

Weak Focusing for Ordered Linear Logic: Robert J. Simmons and Frank Pfenning.
Technical Report CMU-CS-10/147, version of April 2011.
Logical Approximation for Program Analysis: Robert J. Simmons and Frank Pfenning.
Higher-Order and Symbolic Computation.
To appear. Version of April 2011.
Dependent Session Types via Intuitionistic Linear Type Theory: Bernardo Toninho, Luís Caires, and Frank Pfenning.
Submitted, March 2011.
Distributed Deductive Databases, Declaratively The L10 logic programming language: Robert J. Simmons, Bernardo Toninho and Frank Pfenning.
Submitted, February 2011.
Preliminary L10 web page.
Stateful Authorization Logic — Proof Theory and a Case Study: Deepak Garg and Frank Pfenning.
6th International Workshop on Security and Trust Management (STM'10),
Athens, Greece, September 2010.
The original publication is available at www.springerlink.com.
Possession as Linear Knowledge: 3rd International Workshopon Logics, Agents, and Mobility (LAM 2010),
Edinburgh, Scotland, July 2010. [Abstract]
[Slides]
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.
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.
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