Frank Pfenning

Professor of Computer Science	Curriculum Vitæ
Director of Graduate Programs	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	(submitted)

Courses

15-213 Introduction to Computer Systems
Spring'07, 12 units

15-411 Compiler Design
Fall'07, 12 units, Tue,Thu 1:30-2:50, WeH 5310 (tentative)

Conferences

LICS 2008	(PC Chair)	Pittsburgh, Pennsylvania, June 24-27, 2008 Workshops June 22-23, 2008 Short abstracts due January 7, 2008 Extended abstracts due January 14, 2008 Preliminary Call for Papers (PDF)
CADE-21	(PC Chair)	Bremen, Germany, July 17-20, 2007 Workshops July 15-16, 2007 Submissions due February 16, 2007
LICS 2007	(PC Member)	Wroclaw, Poland, July 10-14, 2007 Submissions due January 15, 2007

Organizations

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

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

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)
Intuitionistic Letcc via Labelled Deduction: Jason Reed and Frank Pfenning.
Unpublished manuscript, February 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