Frank Pfenning

President's Professor of Computer Science	Curriculum Vitæ
Head, Department of Computer Science	Short Biography
fp@cs[.cmu.edu]	Picture

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

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

MetaCLF	Formal Reasoning about Languages for Distributed Computation
C0	Specification and Verification in Introductory Computer Science
Certified Interfaces	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-816 Linear Logic
Spring'12, 12 units, MW 12:00-1:20, GHC 4303

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
LFMTP 2011	(PC Member)	Nijmegen, The Netherlands, August 27, 2011 Affiliated with Interactive Theorem Proving (ITP 2011) Abstracts due May 16, 2011 Papers due May 23, 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

Higher-Order Processes, Functions, and Sessions: A Monadic Integration: Bernardo Toninho, Luís Caires, and Frank Pfenning.
European Symposium on Programming (ESOP), pp. 350-369, March 2013.
Behavioral Polymorphism and Parametricity in Session-Based Communication: Luís Caires, Jorge A. Pérez, Frank Pfenning, and Bernardo Toninho.
European Symposium on Programmin (ESOP), pp. 330-349, March 2013.
On Matching Concurrent Traces: Jorge Luis Sacchini, Iliano Cervesato, Frank Pfenning, Carsten Schürmann and Robert J. Simmons.
Working on Unification (UNIF), July 2012.
Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication: Henry DeYoung, Luís Caires, Frank Pfenning, and Bernardo Toninho.
Annual Conference on Computer Science Logic (CSL), pp. 228-242, September 2012.
Church and Curry: Combining Intrinsic and Extrinsic Typing: Talk dedicated to Peter Andrews on the occasion of his retirement.
April 5, 2012.
A related paper paper appeared in:
Reasoning in Simple Type Theory, Festschrift in Honor of Peter B. Andrews on His 70th Birthday, pp. 303-338, College Publications, London, 2008.
Session Types as Intuitionistic Linear Propositions: Luís Caires and Frank Pfenning.
CONCUR 2010, Paris, France, pp. 222-236, Springer LNCS 6269, August 2010.
Extended version available as Technical Report CMU-CS-11-138, December 2012.
Revised version under review, December 2012.
Revised version contains proof details a classical variant of the system.
Towards Concurrent Type Theory: Luís Caires, Frank Pfenning, and Bernardo Toninho.
7th Workshop on Types in Language Design and Implementation (TLDI'12),
Philadelphia, January 2012.
Notes to invited talk (Slides)
Functions as Session-Typed Processes: Bernardo Toninho, Luís Caires, and Frank Pfenning.
15th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'12), pp. 346-360, March 2012.
Termination in Session-Based Concurrency via Linear Logical Relations: Jorge A Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho.
22nd European Symposium on Programming (ESOP'12), 539-558, March 2012.
Proof-Carrying Code in a Session-Typed Process Calculus: Luís Caires, Bernardo Toninho, and Frank Pfenning.
1st International Conference on Certified Programs and Proofs (CPP'11),
pp 21--36, December 2011. Springer LNCS 7086.
Talk Slides
Bottom-Up Logic Programming for Multicores: Flávio Cruz, Michael Ashley-Rollman, Seth Copen Goldstein, Ricardo Rocha, and Frank Pfenning.
Declarative Aspects and Applications of Multicore Programming, Philadelphia, PA, January 2012. To appear as short contribution.
Teaching Imperative Programming With Contracts at the Freshmen Level [Experience Report]: Frank Pfenning, Thomas J. Cortina, and William Lovas.
Unpublished manuscript.
Proof-Carrying Code in a Session-Typed Process Calculus: Luís Caires, Bernardo Toninho, and Frank Pfenning.
1st International Conference on Certified Programs and Proofs (CPP 2011),
December 7-9, 2011, Kenting, Taiwan.
Talk Slides
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 will be available at www.springerlink.com.
Extended version.
Extended and revision journal submission.
Proof-Theoretic Foundations for Programming Languages: Oregon Programming Languages Summer School
Course Materials.
A Proof-Carrying File System with Revocable and Use-Once Certificates: Jamie Morgenstern, Deepak Garg, and Frank Pfenning.
7th International Workshop on Security and Trust Management (STM'11)
To appear. Version of May 2011.
Dependent Session Types via Intuitionistic Linear Type Theory: Bernardo Toninho, Luís Caires, and Frank Pfenning.
Conference on Principles and Practice of Declarative Programming (PPDP'11),
pp. 161-172, Odense, Denmark, July 2011.
Extended version available as Technical Report CMU-CS-11-139, December 2011.

Workshop on Behavioral Types, Lisbon, April 2011.
[Abstract] [Slides]
Distributed Deductive Databases, Declaratively The L10 logic programming language: Robert J. Simmons, Bernardo Toninho and Frank Pfenning.
ACM SIGPLAN X10 Workshop, June 2011. To appear as a short paper.
Preliminary L10 web page. Slightly extended earlier version.
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.
Possession as Linear Knowledge: 3rd International Workshopon Logics, Agents, and Mobility (LAM 2010),
Edinburgh, Scotland, July 2010. Invited Talk.
[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. Invited Talk.
[Abstract]
Refinement Types for Logical Frameworks and Their Interpretation as Proof Irrelevance: William Lovas and Frank Pfenning.
Logical Methods in Computer Science, 6(4), 50pp, December 2010.
A Proof-Carrying File System: Deepag Garg and Frank Pfenning.
Symposium on Security and Privacy (Oakland), pp.349-364, 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