# Robert Harper

**
Professor
**

**Office **
Room 9207
Gates and Hillman Centers

**Email **
rwh@cs.cmu.edu

**Phone **
(412) 268-3675

**Department**

Computer Science Department

**Website **

http://www.cs.cmu.edu/~rwh

**Administrative Support Person **

Ben Cook

**Research Interests**

Formal Methods

Networking

Programming Languages

Security and Privacy

Software Engineering

Pure and Applied Logic

Type Theory

**Advisees**

Harrison Grodin

Yue Niu

## 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.

## Recent Publications

Robert Harper
(
2022
)
*Proceedings of the ACM on Programming Languages*,
**A cost-Aware logical framework
**
*,
Vol.:
6
Issue: (
POPL
)
*

Sterling J, Harper R
(
2022
)
*
Leibniz International Proceedings in Informatics, LIPIcs, *
**Sheaf Semantics of Termination-Insensitive Noninterference
**
*
Vol: 228
*

Robert Harper
(
2021
)
An Equational Logical Framework for Type Theories
*,
Vol.:
*

Cavallo E, Harper R
(
2021
)
*
Logical Methods in Computer Science, *
**Internal parametricity for cubical type theory
**
*
Vol: 17
Issue: (
4
)
*
,
Page(s): 5:1-5:60

Robert Harper
(
2021
)
*Journal of the ACM*,
**Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
**
*,
Vol.:
68
Issue: (
6
)
*
,
Page(s): 1-
47
.