Frank Pfenning

Professor of Computer Science		Curriculum Vitæ
Associate Dean for Graduate Education		Short Biography
School of Computer Science
fp@cs[.cmu.edu]		Picture
		Office:		GHC 9101
Department of Computer Science				Wean Hall 8117
Carnegie Mellon University		Phone:		+1 412 268-6343
Pittsburgh, PA 15213-3891, U.S.A.		Fax:		+1 412 268-3608

Recent Drafts, Talks, and Publications

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.
Submitted, January 2010.

A Concurrent Interpretation of Intuitionistic Linear Logic

Luís Caires and Frank Pfenning.
Submitted, January 2010.

Focus-Preserving Embeddings of Substructural Logics in Intuitionistic Logic

Jason Reed and Frank Pfenning.
Submitted, January 2010.

Refinement Types for Logical Frameworks and Their Interpretation as Proof Irrelevance

William Lovas and Frank Pfenning.
Submitted, November 2009.

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.

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.

A Proof-Carrying File System

Deepak Garg and Frank Pfenning.
Technical Report CMU-CS-09-123, June 2009.
Implementation

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.

A Constructive Approach to the Resource Semantics of Substructural Logics

Jason Reed and Frank Pfenning.
Submitted, April 2009.

A Probabilistic Language Based upon Sampling Functions

Sungwoo Park, Frank Pfenning, and Sebastian Thrun.
TOPLAS, 31(1), December 2008.

Refinement Types as Proof Irrelevance

William Lovas and Frank Pfenning.
To appear at TLCA'09, Brazilia, Brazil, July 2009.

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.

Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic

Sean McLaughlin and Frank Pfenning.
15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'08), pp.174-181, Doha, Qatar, November 2008.
System Description.
Imogen home page

Irrelevance as a Modality

Workshop on Intuitionistic Modal Logics and Applications (IMLA), June 2008.
Invited talk, notes in preparation.

A Bidirectional Refinement Type System for LF

William Lovas and Frank Pfenning.
Proceedings of the 2nd International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, pp. 113-128, Bremen, Germany, July 2007.
Electronic Notes in Theoretical Computer Science (ENTCS), Volume 196, B.Pientka and C.Schürmann, editors.
Extended and revised version available as Technical Report CMU-CS-08-129, May 2008.

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 (to appear).

Linear Logical Algorithms

Robert J. Simmons and Frank Pfenning.
35th International Colloquium on Automata, Languages and Programming (ICALP), July 2008.
To appear.

An Authorization Logic with Explicit Time

Henry DeYoung, Deepak Garg, and Frank Pfenning.
21st Computer Security Foundations Symposium (CSF), June 2008.
Long version with detailed proofs available as Technical Report CMU-CS-07-166.

Intuitionistic Letcc via Labelled Deduction

Jason Reed and Frank Pfenning.
Workshop on Methods for Modalities (M4M), Cachan, France, November 2007.
Revision of January 2008.
(Formalization)

Specifying Properties of Concurrent Computations in CLF

Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker.
Workshop on Logical Frameworks and Metalanguages (LFM'04), Cork, Ireland, July 2004.
Electronic Notes in Theoretical Computer Science (ENTCS), Vol 199C, pp.67-87.
Revised version, October 2007.
Published version at DOI 10.1016/j.entcs.2007.11.013

Subtyping and Intersection Types Revisited

International Conference on Functional Programming (ICFP'07)
Freiburg, Germany, October 1-3, 2007
Invited Talk (Abstract)

Overview of the CMU CSD PhD Program

Talk at the Fall 2007 Immigration Course.

On a Logical Foundation for Explicit Substitutions

Joint invited talk, TLCA and RTA 2007, Paris, France, June 2007.
(Abstract)

Contextual Modal Type Theory

Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka.
Transactions on Computational Logic. To appear.

A Logical Characterization of Forward and Backward Chaining in the Inverse Method

Kaustuv Chaudhuri, Frank Pfenning, and Greg Price.
Submission to special issue in Journal of Automated Reasoning with selected papers from IJCAR 2006, February 2007.

Using Constrained Intuitionistic Linear Logic for Hybrid Robotic Planning Problems

Uluç Saranli and Frank Pfenning.
IEEE International Conference on Robotics and Automation (ICRA'07)
Rome, Italy, April 2007. To appear.

CMU CSD Ph.D. Program Overview

Department of Computer Science Immigration Course, August 2006.
Slides (PDF) Ph.D. Document

Consumable Credentials in Logic-Based Access-Control Systems

Kevin Bowers, Lujo Bauer, Deepak Garg, Frank Pfenning, and Michael Reiter
In Proceedings of the 14th Annual Network and Distributed System Security Symposium (NDSS'07),
San Diego, California, February 2007. To appear.

Avoiding Causal Dependencies via Proof Irrelevance in a Concurrent Logical Framework

Ruy Ley-Wild and Frank Pfenning.
Unpublished manuscript, July 2006.

A Linear Logic of Affirmation and Knowledge

Deepak Garg, Lujo Bauer, Kevin Bowers, Frank Pfenning, and Michael Reiter.
Proceedings of the 11th European Symposium on Research in Computer Security (ESORICS'06)
pp.297-312, Hamburg, Germany, September 2006.

A Logical Characterization of Forward and Backward Chaining in the Inverse Method

Kaustuv Chaudhuri, Frank Pfenning, and Greg Price.
Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR'06),
U. Furbach and N. Shankar, eds, pp. 97-111.
Seattle, Washington, Springer LNCS 4130, August 2006.

Spurious Causal Dependency and Proof Irrelevance

Workshop on Logic Programming and Concurrency, Marseille, France, February 2006.
Invited talk; joint work with Ruy Ley-Wild.

Non-Interference in Constructive Authorization Logic

Deepak Garg and Frank Pfenning.
Proceedings of the 19th Computer Security Foundations Workshop (CSFW'06)
pp.183-293, Venice, Italy, July 2006.
(Formalization)

CLF: A Dependent Logical Framework for Concurrent Computations

Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker.
Unpublished manuscript, July 2004.

A Judgmental Analysis of Linear Logic

Bor-Yuh Evan Chang, Kaustuv Chaudhuri, and Frank Pfenning.
Technical Report CMU-CS-03-131R, April 2003, revised December 2003.
Submitted for publication.

[ Home | Contact | Research | Publications | CV | Students ]
[ Projects | Courses | Conferences | Organizations | Journals ]
[ Logical Frameworks | Pittsburgh Squash Racquets Assocation ]

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