ROBERT HARPER
Professor, Computer Science
www

My principal research interest is in the application of type theory to building and reasoning about programs.  The focus of my work is the ConCert Project, which is led by Karl Crary, Peter Lee, Frank Pfenning, and me. The ConCert Project is concerned with developing the theoretical and practical foundations of trust-free grid computing.  The overall goal is to minimize trust relationships that must hold between host owners and application developers in grid computing.  Our primary methodology is to investigate the use of techniques from logic and type theory to support policy-based certification techniques that allow mutually suspicious parties to verify mechanically the integrity of application code and computed results.  Frank Pfenning and I lead a research project on refinement types, which seek to extend the power of programming language type systems to capture a richer class of invariants without sacrificing the ease of use afforded by current type systems.  I also participate in the Twelf Project on the theory and practice of logical frameworks, and in the Aladdin project on the applications of theory to practical computing.

All of my research centers on the application of type theory to practical programming problems.  Type theory provides a unifying conceptual framework for programming language design, specification, and implementation. As a design tool type theory provides a clean framework for organizing programming language constructs.  A type consists of a collection of values together with a collection of primitive operations on those values. Familiar notions such as trees or lists may be viewed as values of recursive type; the operations permit traversal of these structures.  Procedures may be viewed as values of function type, with operations to create procedures and to apply them to arguments.  Abstract data structures such as dictionaries may be seen as values of existential type, with operations to create a data structure and to use a data structure without revealing its implementation details.  In fact a programming language may be defined by giving an interpretation of its constructs in type theory.  For example, modularity mechanisms might be rendered as uses of existential type, together with a notion of subtyping to admit code reuse and generic operations.  A significant advantage of the type-theoretic viewpoint is that it has direct implications for compiler writers.  My work on the TILT compiler demonstrates the importance of typed intermediate languages for building compilers that generate efficient machine code.  The stages of the TILT compiler are defined as type-directed translations that transform both a program and its type. This allows the compiler to take advantage of type information at compile-, link-, and run-time.  The TILT compiler generates code that is three times faster and uses half the space of other competing compilers.

Types are also a useful tool for prototyping programming languages and proving properties of programs.  My work with Frank Pfenning on the LF logical framework is concerned with the development of a "logic workbench" that allows one to implement formal systems such as type systems for programming languages or logics for reasoning about programs.  The LF language is a simple, yet expressive, type theory in which one may describe the abstract syntax and deductive apparatus of a formal logical system.  The Twelf programming language may be used to build proof checkers and theorem provers for a logic specified in LF.  In a recent case study Twelf was used to define a small assembly language for network packet filters and to define a logic for stating and proving memory invariants of programs written in this language.  The program, together with the LF representation of its proof, form a "self-certified" binary that may be safely installed in an operating system kernel without fear of violating the kernel's memory.  Twelf has also been used to prototype experimental languages, and to study the properties of logical systems such as linear logic.

Home Page: http://www.cs.cmu.edu/~rwh
ConCert Project: http://www.cs.cmu.edu/~concert
Twelf Project: http://www.cs.cmu.edu/~twelf
Aladdin Project: http://www.cs.cmu.edu/~aladdin
Fox Project (completed): http://www.cs.cmu.edu/~fox
TRIPLE Project: http://www.cs.cmu.edu/~triple