Robert Harper - US grants

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 high-level 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 meta-theory 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 meta-languages for their specification have been investigated. These meta-languages are often referred to as logical frameworks. The objective of this effort is to further the theory and practice of logic-independent, computer-assisted formal reasoning and meta-reasoning. This research addresses definitional, operational, and meta-theoretical aspects of logical frameworks comprising work on further design, implementation, and application of such frameworks.

The goal of the project is to demonstrate the feasibility of a broad-based 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 broad-based language it should support both numerical and symbolic computation, should include constructs r parallel programming, and should include the high-level language features found in systems such as Mathematica (e.g. pattern matching, higher-order 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.

CR-0121633
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 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.

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 proof-carrying code, typed intermediate
languages, and typed assembly languages for this purpose. In each
case certificate verification is reduced to type-checking 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.

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.

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.

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 high-level 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.

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 higher-dimensional type
theory, and explore its application to generic programming, a technique
for generating programs from their specifications. Higher-dimensional
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 higher-dimensional 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 computer-verified proofs of mathematical theorems.

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 computing---one 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 Carnegie-Mellon University.

The work is following an end-to-end methodology bridging Church and Turing's theories along with practice. On the theory side, the project is developing a calculus called the ``algorithmic lambda-calculus,'' that equips Church's lambda-calculus 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 Parallel-RAM. 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 lambda-calculus, 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.