Frank Pfenning

Recent Drafts, Talks, and Publications

Distributed System Security via Logical Frameworks

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

Non-Interference in Constructive Authorization Logic

Deepak Garg and Frank Pfenning.
Submitted, October 2005.
(PDF) (Formalization)

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

Contextual Modal Type Theory

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

CMU CSD Ph.D. Program Overview

Department of Computer Science Immigration Course, August 2004.
Slides (PDF) Ph.D. Document

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

Staged Computation with Names and Necessity

Aleksandar Nanevski and Frank Pfenning.
Journal of Functional Programming, to appear.
(PDF)

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)

Substructural Operational Semantics and Linear Destination-Passing Style

Invited talk at the Second Asian Symposium on Programming Languages and Systems (APLAS'04), Taipei, Taiwan, November 2004.
Abstract (PDF) (PS) © Springer-Verlag
Slides (PDF) (PS)

CMU CSD Ph.D. Program Overview

Department of Computer Science Immigration Course, August 2004.
Slides (PDF) (PostScript)
Ph.D. Document

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 Monadic Analysis of Information Flow Security with Mutable State

Karl Crary, Aleksey Kliger, and Frank Pfenning.
Journal of Functional Programming, special issue on Language-Based Security. To appear. (PDF)
Preliminary version presented at the Workshop on Foundations of Computer Security (FCS'04), Turku, Finland, pp.167-184, July 2004.
Summary (PDF) (PS)
Slides (PDF) (PS)

Specifying Properties of Concurrent Computations in CLF

4th International Workshop on Logical Frameworks and Meta-Languages (LFM'04), Cork, Ireland, July 2004.
Joint work with Iliano Cervesato, David Walker, and Kevin Watkins.
(PDF)
Slides (PDF) (PS)

Verifying Uniqueness in a Logical Framework

Penny Anderson and Frank Pfenning.
Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'04), Park City, Utah, pp. 18-33, Sep 2004.
Springer Verlag LNCS 3223. © Springer-Verlag
(PDF)

A Symmetric Modal Lambda Calculus for Distributed Computing

Tom Murphy, Karl Crary, Robert Harper, and Frank Pfenning.
Proceedings of the 19th Annual Symposium on Logic in Computer Science (LICS'04), Turku, Finland, pp.286-295, July 2004. (PDF)
Extended version available as Technical Report CMU-CS-04-105. (PDF)
Formalization of proofs in Twelf (lics04.tar.gz).

Programming Language Overview

Talk at the Computer Science Open House, March 2004.
(slides)

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.

Tridirectional Typechecking

Joshua Dunfield and Frank Pfenning.
31st Annual Symposium on Principles of Programming Languages (POPL'04),
Venice, Italy, pp.281-292, January 2004. (PDF)
Extended version available as Technical Report CMU-CS-04-117, March 2004. (PS) (PDF)

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

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