1993 — 1997 
Pfenning, Frank [⬀] Harper, Robert 
N/AActivity Code Description: No activity code was retrieved: click on the grant title for more information 
Design, Implementation, & Application of a Framework For the Formalization of Deductive Systems @ CarnegieMellon University
TITLE: Design, Implementation, & Application of a Framework Formal deductive systems play a central role in the areas of programming languages and logics. First, they are used to define languages and their semantics at a very highlevel of abstraction (e.g., type systems or operational semantics). Second, they form the basis for the implementation of algorithms pertaining to languages (e.g., type inference or interpretation). Third, they provide a common basis for the study of metatheory of programming languages and logics (e.g., preservation of types under evaluation). Motivated by the tremendous variety of deductive systems of interest in computer science and logic, general metalanguages for their specification have been investigated. These metalanguages are often referred to as logical frameworks. The objective of this effort is to further the theory and practice of logicindependent, computerassisted formal reasoning and metareasoning. This research addresses definitional, operational, and metatheoretical aspects of logical frameworks comprising work on further design, implementation, and application of such frameworks.

1 
1997 — 2002 
Lee, Peter (coPI) [⬀] Miller, Gary (coPI) [⬀] Blelloch, Guy [⬀] Harper, Robert 
N/AActivity Code Description: No activity code was retrieved: click on the grant title for more information 
Advanced Languages For Scientific Computation Environments @ CarnegieMellon University
The goal of the project is to demonstrate the feasibility of a broadbased language for scientific and engineering computation. Such a language should serve equally well for developing production scientific code (which is now typically written in FORTRAN or C) and as the scripting language for interactive scientific computing environments (such as Mathematica or Matlab). This breadth would greatly simplify the development of code by allowing a clean transition from prototyping and small scale experiments to full production code, and would better support the evolution of production code. As a broadbased language it should support both numerical and symbolic computation, should include constructs r parallel programming, and should include the highlevel language features found in systems such as Mathematica (e.g. pattern matching, higherorder functions, and automatic memory management). The project involves demonstrating that it is possible to support these features while maintaining good code efficiency. As such, the project includes work on compiler techniques, on language design, on the development of scientific codes, and experimentation on the codes using the compiler and language. The project is using ML extended with the parallel constructs from NESL as a testbed.

1 
2001 — 2007 
Lee, Peter (coPI) [⬀] Pfenning, Frank (coPI) [⬀] Harper, Robert Crary, Karl [⬀] 
N/AActivity Code Description: No activity code was retrieved: click on the grant title for more information 
Itr/Sy+Si: Language Technology For Trustless Software Dissemination @ CarnegieMellon University
CR0121633 ITR/SY+SI: Language Technology for Trustless Software Dissemination Karl Crary, Robert Harper, Peter Lee, Frank Pfenning
ABSTRACT:
The project investigates the theoretical and engineering basis for the trustless dissemination of software in an untrusted environment. To make this possible the project investigates machinecheckable 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.
To obtain checkable certificates the project develops certifying compilers that equip their object code with formal representations of proofs of properties of the code. Specifically, the project investigates the use of proofcarrying code, typed intermediate languages, and typed assembly languages for this purpose. In each case certificate verification is reduced to typechecking in a suitable type system.
To demonstrate the utility of trustless software dissemination, the project develops an infrastructure for building applications that exploit the computational resources of a network of computers. The infrastructure consists of a "steward" running on host computers that accepts and verifies certified binaries before installing and executing them, and certifying compilers that generate certified binaries for distribution on the network.
The scope of the investigation includes the theory of specification and certification, and the systems building required to implement these ideas.

1 
2007 — 2011 
Pfenning, Frank (coPI) [⬀] Harper, Robert 
N/AActivity Code Description: No activity code was retrieved: click on the grant title for more information 
Collaborative Research: Integrating Types and Verification @ CarnegieMellon University
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 runtime behavior of programs, especially their effect on the execution environment.
To integrate these two methods the project is developing new dependent type systems capable of expressing behavioral specifications and new methods for checking conformance with such rich type constraints. To ensure that the integration is sound, the project is developing its theoretical foundations using mechanized proof assistants. To assess the practicality of the integration, the project is implementing a programming language that integrates types and verification, and is developing applications that illustrate its use.
The primary intellectual contribution of the project is to investigate the design and implementation of programming languages that support the specification and verification of strong correctness properties of programs. A broader contribution of the project is to promote through education the use of formal methods to improve the reliability and maintainability of software systems.

1 
2007 — 2011 
Pfenning, Frank [⬀] Harper, Robert Crary, Karl (coPI) [⬀] 
N/AActivity Code Description: No activity code was retrieved: click on the grant title for more information 
CtT: Collaborative Research: Manifest Security @ CarnegieMellon University
The 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.
Manifest security applies to extensible software platforms, where it addresses two fundamental problems: (1) how to specify policies about what resources an extension may use and how it can handle sensitive data, and (2) how to enforce such policies. The project is developing a novel highlevel logical specification language, encompassing both authorization properties for access control and information flow properties to restrict the use of sensitive data. Adherence to the specification is enforced by a combination of static and dynamic methods, and trustworthiness of the code is established by the explicit representation and verification of formal proofs. Such proofs make the security properties manifest.
Because extensible systems are in widespread use (for example, in web browsers, office software, media players, games, virtual communities, and operating systems) the concept of manifest security has significant potential for broad impact. Rigorous verification methods based on logic and type theory are increasingly important to the software industry; the project advances the use of these methods to ensure security. Results from the research are released via publications and a software platform for secure browser extension, making advances accessible to researchers and practitioners. Results are being integrated into graduate and undergraduate teaching materials as well as courses at summer schools.

1 
2011 — 2015 
Harper, Robert 
N/AActivity Code Description: No activity code was retrieved: click on the grant title for more information 
Shf: Small: Foundations and Applications of HigherDimensional Directed Type Theory @ CarnegieMellon University
A central objective for computer science is to develop methods for building reliable and maintainable software. The most important technique for ensuring these properties is abstraction, the decomposition of a system into separable and reusable components. The theory of abstraction in programming is called type theory. A type is a specification of the behavior of a software component; type checking ensures that programs obey these specifications. This ensures that components can be modified or replaced without fear of disrupting the behavior of other components. By supporting the expression and enforcement of component behaviors, type theory integrates programming with verification, the process of ensuring compliance with specifications. All modern programming languages and development methodologies are based on, or draw inspiration from, type theory. The broad goal of this project is to extend the capabilities of type theory to a wider range of properties, and to use type theory to facilitate the development of reliable software.
Specifically, the research will develop the theory of higherdimensional type theory, and explore its application to generic programming, a technique for generating programs from their specifications. Higherdimensional type theory draws on recent advances in category theory and algebraic topology that emphasize the algebraic structure of relations between programs, and relations between such relations, in direct analogy with the higherdimensional structure of topological spaces. In this setting dependent families of types must respect the algebraic structure of such relations, and in doing so, they implicitly provide transformations that correspond to generic programs whose behavior is determined by their type. More broadly, the project will apply ideas from category theory and topology to improve software development, and apply ideas from type theory to facilitate computerverified proofs of mathematical theorems.

1 
2019 — 2023 
Blelloch, Guy [⬀] Harper, Robert Acar, Umut (coPI) [⬀] 
N/AActivity Code Description: No activity code was retrieved: click on the grant title for more information 
Shf: Medium: Algorithmic LambdaCalculus For the Design, Analysis, and Implementation of Parallel Algorithms @ CarnegieMellon University
The hardware advances of recent years have brought multicore chips and parallel computing to the mainstream. While there have been many advances in parallel software for such multicore chips over the past decade, there is still no satisfactory model for analyzing the performance of parallel algorithms. In particular, and unlike the case for sequential algorithms, there is a gap between cost models for estimating performance of algorithms and easy to use programming models for implementing the algorithms. This project is developing a practical approach to parallel algorithms by bringing together two fundamental but distinct theories of computingone based on machine models and following the work that dates back to Dr. Alan Turing, and the other based on language models and following the work that dates back to Dr. Alonzo Church. The novelty of the project is in combining these two theories, for which there is currently a large rift. The impact of the project is in making significant steps in simplifying the design and analysis of parallel algorithms, and better understanding of the relationship between the two theories of computing. The educational component of this project involves teaching undergraduates parallel algorithms and creates ample opportunities to test the practical effectiveness of the proposed approach, along with concrete efforts to broaden participation in computing through programs at CarnegieMellon University.
The work is following an endtoend methodology bridging Church and Turing's theories along with practice. On the theory side, the project is developing a calculus called the ``algorithmic lambdacalculus,'' that equips Church's lambdacalculus with a cost semantics, making it possible to reason about the total work and parallel span (time) of programs, which in turn can be used to understand the performance of algorithms, at least asymptotically. To show that this calculus is realizable, the project is theoretically establishing that the calculus is faithful to a transition semantics, which can then be efficiently realized on an abstract machine such as the ParallelRAM. On the practical side, the project is developing a programming language and a compiler that faithfully implements this theory. The project is also extending the algorithmic lambdacalculus, the realizability theorems, and the implementation to support important features such as aggregate parallel data structures, interaction, and different forms of parallelism.
This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

1 