Robert Harper Professor Website ORCiD Office 9207 Gates and Hillman Centers Email rwh@cs.cmu.edu Phone (412) 268-3675 Department Computer Science Department Administrative Support Person 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 CSD Courses Taught 15791 - Spring, 2024 Research/Teaching 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. Publications Journal Article Decalf: A Directed, Effectful Cost-Aware Logical Framework 2024 • Proceedings of the ACM on Programming Languages • 8: Grodin H, Niu Y, Sterling J, Harper R Conference A Metalanguage for Cost-Aware Denotational Semantics 2023 • Proceedings - Symposium on Logic in Computer Science • 2023-June: Niu Y, Harper R Preprint A Verified Cost Analysis of Joinable Red-Black Trees 2023 Li R, Grodin H, Harper R Conference Amortized Analysis via Coinduction 2023 • Leibniz International Proceedings in Informatics • 270: Grodin H, Harper R Preprint Amortized Analysis via Coinduction 2023 Grodin H, Harper R
Journal Article Decalf: A Directed, Effectful Cost-Aware Logical Framework 2024 • Proceedings of the ACM on Programming Languages • 8: Grodin H, Niu Y, Sterling J, Harper R
Conference A Metalanguage for Cost-Aware Denotational Semantics 2023 • Proceedings - Symposium on Logic in Computer Science • 2023-June: Niu Y, Harper R
Conference Amortized Analysis via Coinduction 2023 • Leibniz International Proceedings in Informatics • 270: Grodin H, Harper R
