Frank Pfenning

Contents Current: Session Types | C0
  Past: MetaCLF | Certified Interfaces | Twelf | Prospero | Manifest Security | Logosphere | SeLF | Triple | ConCert | Staged Computation | Proof Search | Fox | Types in Programming | Ergo


Session Types: Structured Message-Passing Concurrency

This project aims at understanding message-passing concurrency through session types, which are closely related to linear logic and other substructural logics. This line of research started with a joint paper Session Types as Intuitionistic Linear Propositions (with Luís Caires, CONCUR 2010). Most of my publications 2011-2018 are concerned with some aspect of session types and concurrency. Introductory material:

C0: Specification and Verification in Introductory Computer Science

Principal Investigators Frank Pfenning (Carnegie Mellon University)
Support MSR-CMU Center for Computational Thinking; Google

C0 is a small safe subset of the C programming language, augmented with contracts, specifically developed for teaching the course 15-122 Principles of Imperative Computation at Carnegie Mellon University.


MetaCLF: Formal Reasoning about Languages for Distributed Computation

Principal Investigators Iliano Cervesato (Carnegie Mellon University - Qatar)
Frank Pfenning (Carnegie Mellon University)
Support NPRP 09-1107-1-168, Qatar National Research Foundation

This project aims at developing recent work on language specification with substructural operational semantics (SSOS) into methodologies for designing and reasoning about programming and specification languages for distributed computation. We use of the Concurrent Logical Framework (CLF) in order to elegantly implement SSOS specifications, and to develop and implement (co)inductive techniques to reason about such specification.

Certified Interfaces: Certified Interfaces for Integrity and Security in Web-based Applications

Principal Investigators Luís Caires (Universidade Nova de Lisboa)
Frank Pfenning (Carnegie Mellon University)
Vasco Vasconcelos (Universidade de Lisboa)
Carlos Alves (OutSystems, SA)
Lúcio Ferrao (OutSystems, SA)
Support NGN-44, CMU|Portugal and FCT, Portugal, 5/1/2009-4/30/2012

The project aims at the development of new techniques for enforcing security, integrity, and correctness requirements on distributed extensible web-based applications by introducing novel, semantically rich notions of interface description languages, based on advanced type systems and logics.

Prospero: Integrating Types and Specifications

Principal Investigators Robert Harper, Frank Pfenning (CMU)
Greg Morrisett (Harvard)
Support NSF-0702381

The project investigates the integration of types and verification as complementary techniques for building robust, reliable, and maintainable software. Types provide the foundation for the composition of systems from independently reusable components by providing a rich language of invariants governing programs and data. Verification provides the foundation for reasoning about the run-time behavior of programs, especially their effect on the execution environment.

Manifest Security: Logics and Languages for Manifestly Secure Systems

Principal Investigators Karl Crary, Robert Harper, Frank Pfenning (CMU)
Benjamin Pierce, Stephanie Weirich, Steve Zdancewic (UPenn)
Support NSF-0716469 and NSF-0715936

This project proposes manifest security as a new architectural principle for secure extensible systems. Its research objectives are to develop the theoretical foundations for manifestly secure software and to demonstrate its feasibility in practice.

SeLF: Distributed System Security via Logical Frameworks

Principal Investigators Lujo Bauer (CyLab, CMU)
Frank Pfenning
Mike Reiter (University of North Carolina)
Support ONR MURI N00014-04-1-0724, 2004-2006;
IARPA 2007-2008
Keywords Distributed Systems, Security , Logical Framework

We are conducting a research program with the goal of advancing security in distributed systems via the application of logical frameworks. Our work targets multiple facets of the life-cycle of a distributed system, ranging from design through execution, and from sound mechanism design through sound policy enforcement.

Logosphere: A Formal Digital Library

Principal Investigators Carsten Schürmann (Yale University)
Frank Pfenning, Michael Kohlhase (CMU)
Natarajan Shankar, Sam Owre (SRI International)
Support NSF CCR-ITR-0325808, 2003-2008
Keywords Digital Library, Logical Framework

Mathematical knowledge is at the core of science and engineering. The quantity of mathematical knowledge is growing faster than our ability to formalize and organize it. The proposed research focuses on developing a Formal Digital Library called Logosphere, a common and open infrastructure for managing and sharing mathematical knowledge and formal proof. Central to this work is the design of a logical framework as a representation language for logical formalisms, individual theories, and proofs, with an interface to theorem proving systems such as PVS or HOL, that have been effective in industrial practice. Logosphere emphasizes interoperability between theorem proving systems, and the exchange and reusability of mathematical facts across different systems. The Logosphere infrastructure is designed to be scalable with respect to the size of the knowledge base as well as the diversity of formalisms.

The Triple Project: Type Refinements in Programming Languages

Principal Investigators Robert Harper, Frank Pfenning
Support NSF CCR-0204248, 2002-2005
Keywords Refinement Types

Research in the Triple project centers on the extension of syntactic type disciplines with a level of refinements that isolate properties of a type. Properties of interest include representation invariants on data structures, value range invariants, and state invariants which govern changes to mutable storage. Crucially, refinements are formally declared by the programmer, and rigorously checked by a mechanical refinement checker. This allows properties to be stated at module boundaries, and allows the programmer to ascertain that critical properties hold at specified points in a program.

The ConCert Project: Language Technology for Trustless Software Dissemination

Principal Investigators Karl Crary, Robert Harper, Peter Lee, Frank Pfenning
Support NSF 0121633 ITR/SY+SI, 2001-
Keywords Certified Code, Grid Computing

The ConCert Project investigates the theoretical and engineering basis for the trustless dissemination of software in an untrusted environment. To make this possible the project investigates machine-checkable certificates of compliance with security, integrity, and privacy requirements. Such checkable certificates allow participants to verify the intrinsic properties of disseminated software, rather than extrinsic properties such as the software's point of origin.

The Twelf Project: Logical and Meta-Logical Frameworks

Principal Investigator Frank Pfenning
Current Support NSF CCR-9988281 2000-2002
Prior Support NSF CCR-9619584 1997-1999, NSF CCR-9303383 1993-1996
Keywords LF Logical Framework, Elf, Twelf

The objective of the Twelf Project is to design, implement, and apply a comprehensive meta-language and environment for the formalization, implementation and meta-theory of deductive systems. This includes specification and reasoning about programming languages and logic. We refer to the current implementation as the Twelf meta-logical framework.

Staged Computation

Principal Investigators Peter Lee and Frank Pfenning
Support NSF CCR-9619832, 1997-2000
Keywords Run-time code generation, modal ML

The research of the Staged Computation project is aimed at developing language designs and compiler technology to exploit the notion of staged computation to increase performance without sacrificing adaptability, modularity or safety. The language design is based primarily on type theory for modal logic; the implementation technology is based primarily on run-time code generation.

Proof Search in Logical Frameworks

Principal Investigators Dieter Hutter, DFKI Saarbrücken
Frank Pfenning, Carnegie Mellon University
Support NSF INT-9909952, 2000-2003, and DAAD
Keywords Logical frameworks, inductive theorem proving, formal methods

To date, the emphasis in the development of logical frameworks has been on ease of specification, proof representation, and meta-programming with a relatively low degree of automation. The central objective of this collaboration is to further our understanding of how standard techniques of redundancy elimination, efficient implementation, and heuristic search from specific logics can be generalized and applied to logical frameworks. We plan to validate our design with implementations in the setting of the INKA and VSE systems at the DFKI and University of Saarbrücken and the Twelf system at Carnegie Mellon University. Intended application domains include formal methods and inductive reasoning about programming languages and logics.

The Fox Project: Advanced Language Technology for Extensible Systems

Principal Investigators Robert Harper, Peter Lee, Frank Pfenning
Support Advanced Research Projects Agency CSTO, ARPA Order No. C533
1996-1998, 1999-2001
Keywords The FoxNet, Typed Intermediate Languages, Proof-Carrying Code

The objective of the Fox Project in the School of Computer Science at Carnegie Mellon is to advance the art of programming language design and implementation, and simultaneously to apply principles of programming languages to advance the art of systems building. The work of the project includes theoretical studies of programming languages and their properties, development of new compiler and run-time technology, and empirical studies of the application of advanced language techniques to real-world programming problems, especially in the areas of high-performance networks and operating systems.

Types in Programming

Principal Investigators John Reynolds and Dana Scott
Support DARPA, 1990-1993
Keywords Types, Programming Languages, Semantics

The Ergo Project: Semantically-Based Program Design Environments

Principal Investigators Bill Scherlis and Dana Scott
Support DARPA and ONR, 1986-1991
Keywords Program Transformation, Environment, Meta-Languages

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

Frank Pfenning