Frank Pfenning

Professor of Computer Science	Curriculum Vitæ
	Short Biography
fp@cs[.cmu.edu]	Picture

Department of Computer Science	Office:	Wean Hall 8117
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 Publications, Students & Co-authors)

Projects

Logosphere	A Formal Digital Library
Triple	Type Refinement in Programming Languages
ConCert	Language Technology for Trustless Software Dissemination
Twelf	Logical and Meta-Logical Frameworks
SeLF	Distributed System Security via Logical Frameworks
Manifest Security	Logics and Languages for Manifestly Secure Systems
Prospero	Integrating Types and Specifications

Courses

15-317 Constructive Logic
Fall'08, 12 units, TuTh 12:00-1:20

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

Conferences

POPL 2009	(PC Member)	Savannah, Georgia, Jan 21-23, 2009 Abstract submission July 8, 2008, 5pm EDT Paper submission July 15, 2008, 5pm EDT
LICS 2008	(PC Chair)	Pittsburgh, Pennsylvania, June 24-27, 2008 Workshops June 22-23, 2008 Colocated with CSF 2008, June 23-25, 2008

Organizations

CADE	Trustee and Former President	(Conference on Automated Deduction)
GPCE	Former SC Member	(Generative Programming and Component Engineering)
PPDP	Former SC Member	(Principles and Practice of Declarative Programming)
MPII	Advisory Board Chair	(Max-Planck-Institut für Informatik, Saarbrücken)

Journals

TCS	Editor	(Theoretical Computer Science)
JAR	Editor	(Journal of Automated Reasoning)
JSC	Editor	(Journal of Symbolic Computation)

Home Pages

Logical Frameworks

CMU Squash Ladder

PSRA Box League

Recent Drafts, Talks, and Publications

Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic: 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'08), Doha, Qatar, November 2008. To Appear.
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.

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