Frank Pfenning

President's Professor of Computer Science   Curriculum Vitæ    Frank Pfenning
Head, Department of Computer Science   Short Biography
fp@cs[]   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)
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
15-411/611 Compiler Design
Fall'14, 12 units, TuTh 9:00am-10:20am, WeH 7500

Recent Drafts, Talks, and Publications

Polarized Substructural Session Types
Frank Pfenning and Dennis Griffith.
18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2015),
London, UK, April 2015. To appear.
Invited talk.
Proof Theory and Its Role in Programming Language Research
Programming Languages Mentoring Workshop (PLMW 2015),
Mumbai, India, January 2015
From Linear Logic to Session-Typed Concurrent Programming
Tutorial at POPL 2015, Mumbai, India, January 2015
Joint work with Luís Caires, Bernardo Toninho, and Dennis Griffith
Live code: primes.sill queue-data.sill
SILL implementation in OCaml:
Corecursion and Non-Divergence in Session-Typed Processes
Bernardo Toninho, Luís Caires, and Frank Pfenning.
9th International Symposium on Trustworthy Global Computing (TGC 2014)
Rome, Italy, September 2014. To appear.
A Linear Logic Programming Language for Concurrent Programming over Graph Structures
Flávio Cruz, Ricardo Rocha, Seth Goldstein, and Frank Pfenning.
30th International Conference on Logic Programming (ICLP 2014)
Vienna, Austria, July 2014. To appear. Best paper award.
Book Review: Programming with Higher-Order Logic
by Dale Miller and Gopalan Nadathur, Cambridge University Press, 2012.
Theory and Practice of Logic Programming 14(2), pp. 265-267.
© Cambridge University Press. Definitive version
Concurrent Programming in Linear Type Theory
Mathematical Structures of Computation
Lyon, February 2014.
Earlier version presented at the ABCD Project Meeting.
Imperial College, London, January 2014.
Logic-Based Domain-Aware Session Types
Luís Caires, Jorge A. Pérez, Frank Pfenning, and Bernardo Toninho.
Linear Logical Relations and Observational Equivalences for Session-Based Concurrency
Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho.
A revised version has been accepted to Information & Computation.
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.
Complete list of publications

Older Unpublished Drafts and Talks

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.
Teaching Imperative Programming with Contracts at the Freshmen Level [Experience Report]
Frank Pfenning, Thomas J. Cortina, and William Lovas.
Unpublished manuscript, September 2011.
Possession as Linear Knowledge
3rd International Workshopon Logics, Agents, and Mobility (LAM 2010),
Edinburgh, Scotland, July 2010. Invited Talk.
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.

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