Frank Pfenning
Projects

Prospero:
Integrating Types and Specifications

Manifest Security:
Logics and Languages for Manifestly Secure Systems

SeLF:
Distributed System Security via Logical Frameworks

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

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

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

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

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

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

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

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

The Ergo Project:
Semantically-Based Program Design Environments

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

Frank Pfenning