Frank Pfenning

Professor of Computer Science		Curriculum Vitæ
School of Computer Science		Short Biography
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

Recent Drafts, Talks, and Publications

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), March 2012.
To appear. Preliminary version of October 2011.

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), March 2012.
To appear. Preliminary version of October 2011.

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.
Rejected from SIGCSE'12. The program chairs have provided no explanation for a meta-review that included the following:

The most significant weakness was that it was too demanding for many schools to try it ("The paper describes in detail the course's learning objectives from three points of view: computational thinking, programming skills, and data structures and algorithms. Perhaps the only comment here is that the course expects a lot from the students.")

One has to wonder how SIGCSE can further computer science education with this prevailing attitude regarding a challenging innovative course that has been successfully taught to 220 freshmen, roughly evenly divided between majors and nonmajors.

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.

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)
To appear.

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]

Session Types as Intuitionistic Linear Propositions

Luís Caires and Frank Pfenning.
CONCUR 2010, Paris, France, pp. 222-236, Springer LNCS 6269, August 2010.

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.

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

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