Frank Pfenning

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

Courses

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

15-312 Foundations of Programming Languages
Fall'04, 12 units (Version from Fall'03)

Conferences

RTA 2005	(PC Member)	Nara, Japan, Apr 18-21, 2005
LICS 2005	(PC Member)	Chicago, Illinois, Jun 25-Jul 1, 2005
TPHOLs 2005	(PC Member)	Submissions due Feb 18, 2005
CADE 2005	(PC Member)	Submissions due Feb 25, 2005
FCS 2005	(PC Member)	Submissions due Mar 18, 2005
ICFP 2005	(PC Member)	Submissions due Apr 13, 2005
IMLA 2005	(PC Co-Chair)	Submissions due Apr 17, 2005

Organizations

CADE	Former Trustee and 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

JAR	Editor	(Journal of Automated Reasoning)
JSC	Editor	(Journal of Symbolic Computation)
JFLP	Editor	(Journal of Functional and Logic Programming)

Home Pages

Logical Frameworks

CMU Squash Ladder

Pittsburgh Squash Racquets Association

Recent Drafts, Talks, and Publications

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.
Submitted, 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.
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, Sep 2004. To appear. (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.
Review of Types and Programming Languages: Benjamin C. Pierce, The MIT Press, Cambridge, Massachusetts, xxi + 623 pp, 2002.
Journal of Symbolic Logic, to appear. (PDF)
A Linear Spine Calculus: Iliano Cervesato and Frank Pfenning.
Journal of Logic and Computation, pp. 639-688, Vol. 13, No. 5, 2003.
(PDF) © Oxford University Press.
Proceedings of the Second international Conference on Generative Programming and Component Engineering: Frank Pfenning and Yannis Smaragdakis, editors.
Erfurt, Germany, September 22-25, 2003.
Springer-Verlag LNCS 2830. © Springer-Verlag
Available in the ACM Digital Library.
Available through LNCS Online.
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)
Proofs R Us: Talk at the workshop on the NSF supported Logosphere and Infer! projects.
SRI International, October 2003. (PS)
A Concurrent Logical Framework: The Propositional Fragment: Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker.
January 2004, to appear in TYPES'03, Springer-Verlag LNCS 3085. (PDF)
Programming Language Overview: Talk at the Computer Science Immigration Course, August 2003.
(slides)
A Modal Foundation for Meta-Variables: Aleksandar Nanevski, Brigitte Pientka, and Frank Pfenning.
Preliminary Proceedings of the Second ACM SIGPLAN Workshop on Mechanized Reasoning about Languages with Variable Binding (MERLIN'03), Uppsala, Sweden, August 2003.
Paper on work in progress (Category B). (PDF)
On Order and Linearity in Logical Frameworks: The Lambek Calculus Revisited: Workshop on Logic and Computational Linguistic, Ottawa, Canada, June 2003.
Joint work with Jeff Polakow and Kevin Watkins.
Slides (PDF) (PS)
Linear Destination Passing as a Modular Semantic Framework: Internal work-in-progress talk at ConCert project meeting, May 2003.
Slides (PDF) (PS)
A Coverage Checking Algorithm for LF: Carsten Sch�rmann and Frank Pfenning.
Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003)
D. Basin and B. Wolff, eds., pp. 120-135, Rome, Italy, September 2003.
(PDF) © Springer-Verlag LNCS 2758
A Concurrent Logical Framework II: Examples and Applications: Iliano Cervesato, Frank Pfenning, David Walker, and Kevin Watkins.
Technical Report CMU-CS-02-102, March 2002, revised May 2003. (PDF)
A Concurrent Logical Framework I: Judgments and Properties: Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker.
Technical Report CMU-CS-02-101, March 2002, revised May 2003. (PDF)
A Concurrent Logical Framework: Workshop Types 2003, Turin, Italy, May 2003.
Joint work with Iliano Cervesato, David Walker, and Kevin Watkins.
Slides (PDF) (PS)
A Learning Algorithm for Localizing People Based on Wireless Signal Strength that Uses Labeled and Unlabeled Data: M. Berna, B. Lisien, B. Sellner, G. Gordon, F. Pfenning, and S. Thrun.
18th International Joint Conference on Artificial Intelligence (IJCAI'03), Acapulco, Mexico, August 2003.
To appear as poster.
A Monadic Probabilistic Language: Sungwoo Park, Frank Pfenning, and Sebastian Thrun.
Draft manuscript, March 2003. (PDF)
A Type Theory for Memory Allocation and Data Layout: Leaf Petersen, Robert Harper, Karl Crary, and Frank Pfenning.
Conference Record of the 30th Symposium on Principles of Programming Languages (POPL'03),
Greg Morrisett, editor, pp. 172-184. New Orleans, Louisiana, January 2003. (PDF)
Extended version available as Technical Report CMU-CS-02-171, December 2002. (PDF).
Meta-Programming with Names and Necessity: Aleksandar Nanevski and Frank Pfenning.
Submitted, February 2003. (PDF)
Resource Management for the Inverse Method in LInear Logic: Kaustuv Chaudhuri and Frank Pfenning.
Draft manuscript, January 2003. (PDF)
Optimizing Higher-Order Pattern Unification: Brigitte Pientka and Frank Pfenning.
Proceedings of the 19th International Conference on Automated Deduction (CADE-19), Miami Beach, Florida
F. Baader, ed., pp 473-487, Springer Verlag LNAI 2741, July 2003.
(PDF) © Springer-Verlag
Slides (PS) (PDF)
Type Assignment for Intersections and Unions in Call-by-Value Languages: Joshua Dunfield and Frank Pfenning.
Proceedings of the 6th International Conference on Foundations of Software Science and Computational Structures (FOSSACS'03), Warsaw, Poland.
A.D. Gordon, editor, pp 250-266, Springer-Verlag LNCS 2620, April 2003. (PDF) © Springer-Verlag

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