Robert Harper
Office 9207 Gates and Hillman Centers
Email rwh@cs.cmu.edu
Phone (412) 268-3675
Department
Computer Science Department
Administrative Support Person
Ben Cook
Oliver Moss
Research Interests
Formal Methods
Networking
Programming Languages
Security and Privacy
Software Engineering
Pure and Applied Logic
Type Theory
Advisees
Harrison Grodin
Yue Niu
Teaching/Research Statement
The goal of my research is to develop a comprehensive theory of programming that integrates with the practice of software development. The premise of my research is that programming is an explanatory activity, a form of expression intended to convey an idea that is both comprehensible by other people and executable by a computer. Language therefore plays a central role in programming. The overall goal of my work is to develop a language for computation that serves both purposes.
The focus of my work is on the development and application of type theory as the language of computation. As the name implies, the central organizing principle of type theory is the concept of a type. For example, familiar tree and graph structures may be viewed as instances of the general concept of an inductive type, infinitary data structures such as streams of values may be viewed as coinductive types, and language features such procedures or objects may be viewed as instances of the general concept of a function. A beauty of type theory is that it provides a rich framework that accounts not only for the computational aspects of programming, but also the reasoning involved in ensuring that a program behaves correctly. The main tool is the propositions-as-types principle in which specifications, or propositions, are identified with types, and proofs are identified with programs. A proof, after all, is a step-by-step procedure for transforming assumptions into conclusions; it is, therefore, a program that takes assumptions as inputs and produces proofs as outputs. The theorem statement is a specification, or type, of this input-output behavior. Another beauty is that type theory connects directly to the language of mathematics through the concept of a category, a very general kind of algebraic structure. Types correspond to structures, such as topological spaces, and programs correspond to structure-preserving mappings between them. This provides a pathway for integrating the language of mathematics with the language of programming.