Frank Pfenning
Projects

Current

Session Types: Structured Concurrency

This project aims at understanding message-passing (and recently also shared memory 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-2020 are concerned with some aspect of session types and concurrency. Some introductory material:

• Session-Typed Concurrent Programming, short course (5 lectures) at the Oregon School on Programming Languages, 2019.
• Message-Passing Concurrency and Substructural Logics, tutorial, POPL 2018 (live-coded examples)
• Manifest Sharing with Session Types, ICFP 2017.
• Substructural Logics, course materials, Fall 2016 (combined lecture notes)

C0: Specification and Verification in Introductory Computer Science

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.

Past

MetaCLF: Formal Reasoning about Languages for Distributed Computation

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

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

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

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

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 ]

Frank Pfenning