|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|
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:
|Principal Investigators||Stephanie Balzer and Frank Pfenning|
|Support||NSF Award 1718267, Enriching Session Types for Practical Concurrent Programming, 7/1/2019-6/30/2020|
|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.
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.
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.
Robert Harper, Frank Pfenning (CMU)
Greg Morrisett (Harvard)
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.
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.
Lujo Bauer (CyLab, CMU)
Mike Reiter (University of North Carolina)
|Support|| ONR MURI N00014-04-1-0724, 2004-2006;
|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.
|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.
|Principal Investigators||Robert Harper, Frank Pfenning|
|Support||NSF CCR-0204248, 2002-2005|
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.
|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.
|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.
|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.
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.
|Principal Investigators||Robert Harper, Peter Lee, Frank Pfenning|
|Support|| Advanced Research Projects Agency CSTO, ARPA Order No. C533
|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.
|Principal Investigators||John Reynolds and Dana Scott|
|Keywords||Types, Programming Languages, Semantics|
|Principal Investigators||Bill Scherlis and Dana Scott|
|Support||DARPA and ONR, 1986-1991|
|Keywords||Program Transformation, Environment, Meta-Languages|