Robert Harper's Home Page

Robert Harper
Computer Science Department	Phone	+1 (412) 268-3675
Carnegie Mellon University	EMail	`rwh@cs.cmu.edu`
	PGP	Public Key
5000 Forbes Avenue	Office	9207 Gates-Hillman Center
Pittsburgh, PA 15213-3890	Assistant	Oliver Moss (6006 GHC)

Papers

Amortized Analysis via Coalgebra. Harrison Grodin and Robert Harper. MFPS 2024 Paper. MFPS 2024 Slides.
Cost-sensitive computational adequacy of higher-order recursion in synthetic domain theory. Yue Niu, Jonathan Sterling, and Robert Harper. MFPS 2024 Paper. MFPS 2024 Talk.
Decalf: A Directed, Effectful Cost-Aware Logical Framework. Harrison Grodin, Robert Harper, Yue Niu, and Jonathan Sterling. POPL 2024.
A verified cost analysis of joinable red-black trees. Runming Li, Harrison Grodin, and Robert Harper. October, 2023.
A metalanguage for cost-aware denotational semantics. Yue Niu and Robert Harper. LICS 2023.

Talks

Integrating Cost and Behavior in Type Theory. Morgenstern Colloquium, INRIA and Université Côte d'Azur, Sophia-Antipolis, October, 2023.
Integrating Cost and Behavior in Type Theory. Plenary invited lecture CALCO/MFPS, Bloomington, June, 2023. (See also LIPIcs Vol 270 CALCO 2023.)

Students

Harrison Grodin. Cost-Aware Logical Frameworks.
Runming Li Cost-Aware Compiler Correctness.

Collaborators

Umut Acar. Parallel programming.
Stephanie Balzer. Session types for concurrency.
Guy E. Blelloch. Parallelism, cost semantics, integrating algorithms and programming languages.
Karl Crary. Certifying compilers, logical frameworks, mechanized metatheory.
Max Planck Institute for Software Systems, Kaiserslautern and Saarbruecken, Germany. External Scientific Member.

Books

Robert Harper. Practical Foundations for Programming Languages (Second Edition)
Robert Harper. Programming in Standard ML, 2013.
Robert Harper (editor). Types in Compilation. Springer-Verlag Lecture Notes in Computer Science, 2001.
Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.
(Available at SML Family Web Site.)

Courses

Honors and Awards

ACM SIGPLAN Programming Languages Achievement Award, 2021.
IEEE Symposium on Logic in Computer Science Test of Time Award, 2007.
ACM SIGPLAN Most Influential PLDI Paper Award, 2006.
ACM Fellow, 2005.
Allen Newell Award for Research Excellence, School of Computer Science, Carnegie Mellon University, 2001.
Herbert A. Simon Award for Teaching Excellence in Computer Science, School of Computer Science, Carnegie Mellon University, 2001.

Conferences and Workshops

IFIP WG2.8 Working Group on Functional Programming

Journals

Editorial Board, Foundations and Trends in Programming Languages.

Web Sites

Red* Family of proof assistants
SML Family of functional programming languages.
Twelf implementation of the LF logical framework.

Research Funding

AFOSR under MURI grant FA9550-21-0009, Tristan Nguyen, program manager.
AFOSR under award number FA9550-21-1-0385, Tristan Nguyen, program manager.
NSF grant CCF-1901381, "Algorithmic λ-Calculus for the Design, Analysis, and Implementation of Parallel Algorithms."

Last modified: