Frank Pfenning

Recent Drafts, Talks, and Publications

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

Avoiding Causal Dependencies via Proof Irrelevance in a Concurrent Logical Framework

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

A Linear Logic of Affirmation and Knowledge

Deepak Garg, Lujo Bauer, Kevin Bowers, Frank Pfenning, and Michael Reiter.
April 2006. Revised version to appear at ESORICS 2006.
(PDF)

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.
(PDF)

Spurious Causal Dependency and Proof Irrelevance

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

Intuitionistic Letcc via Labelled Deduction

Jason Reed and Frank Pfenning.
Unpublished manuscript, February 2006.
(PDF) (Formalization)

Non-Interference in Constructive Authorization Logic

Deepak Garg and Frank Pfenning.
Proceedings of the 19th Computer Security Foundations Workshop (CSFW'06)
Venice, Italy, July 2006. To appear.
(PDF) (Formalization)

Consumable Credentials in Logic-Based Access Control

Lujo Bauer, Kevin D. Bowers, Frank Pfenning, and Michael K. Reiter
Technical Report CMU-CYLAB-06-002, February 2006.

Distributed System Security via Logical Frameworks

Colloquium talk at McGill University, November 2005.
Slides (PowerPoint)

Towards a Type Theory of Contexts

Invited talk at Workshop on Mechanized Reasoning about Languages with Variable Binding (Merλin'05), Tallinn, Estonia, September 2005.
Abstract (PDF)
Slides (PDF) (PS)

Contextual Modal Type Theory

Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka.
Submitted, September 2005.
(PDF)

Constructive Authorization Logics

Invited talk at the 4th Workshop on Foundations of Computer Security (FCS'05), Chicago, Illinois, July 2005.
Slides (PDF) (PS)

Linear Logical Algorithms

Workshop on Programming Logics in Memory of Harald Ganzinger, Saarbrücken, Germany, June 2005.
Slides (PDF) (PS)

Type-Directed Concurrency

Deepak Garg and Frank Pfenning.
16th International Conference on Concurrency Theory (CONCUR'05), San Francisco, California, pp.6-20, August 2005.
Springer Verlag LNCS 3653.
(PDF)

Focusing the Inverse Method for Linear Logic

Kaustuv Chaudhuri and Frank Pfenning.
14th Annual Conference on Computer Science Logic (CSL'05), Oxford, England, L.Ong, ed., pp.200-215, August 2005.
Springer Verlag LNCS 3634
(PDF)
Implementation

The Computer Science Ph.D. Program

Department of Computer Science Open House, March 2005.
Slides (PDF)
Ph.D. Document

A Focusing Inverse Method Prover for First-Order Linear Logic

Kaustuv Chaudhuri and Frank Pfenning.
20th International Conference on Automated Deduction (CADE-20), Tallinn, Estonia, R.Nieuwenhuis, ed., pp.69-83, July 2005.
Springer Verlag LNCS 3632. © Springer-Verlag (SpringerLink)
(PDF)
Propositional and first-order prover implementations

Monadic Concurrent Linear Logic Programming

Pablo López, Frank Pfenning, Jeff Polakow, and Kevin Watkins.
7th International Symposium on Principles and Practice of Declarative Programming, Lisbon, Portugal, pp.35-46, July 2005.
(PDF)
Prototype implementation

Distributed System Security via Logical Frameworks

Invited talk at the 5th Workshop on Issues in the Theory of Security (WITS'05)
Long Beach, California, January 2005.
Slides (PDF) (PS)

A Probabilistic Language based upon Sampling Functions

Sungwoo Park, Frank Pfenning, and Sebastian Thrun.
32nd Annual Symposium on Principal of Programming Languages (POPL'05), Long Beach, California, January 2005, pp.171-182.
(PDF)
Extended version available as Technical Report CMU-CS-04-173, November 2004.

CLF: A Dependent Logical Framework for Concurrent Computations

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

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. (PDF)
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