Papers

• Recursive Logical Relations for Intuitionistic Linear Session Types. Stephanie Balzer, Farzaneh Derakhshan, Robert Harper, and Yue Yao. Preprint, October, 2025.
• Mechanizing Synthetic Tait Computability in Istari. Runming Li, Yue Yao, and Robert Harper. To appear, CPP 2026.
• Abstraction Functions as Types. Harrison Grodin, Runming Li, and Robert Harper. To appear, ACM PoPL 2026.
• Canonicity for Cost-Aware Logical Framework via Synthetic Tait Computability. Runming Li and Robert Harper. Preprint, April, 2025.
• Amortized Analysis via Coalgebra. Harrison Grodin and Robert Harper. MFPS XL, December, 2024.
• Cost-sensitive computational adequacy of higher-order recursion in synthetic domain theory. Yue Niu, Jonathan Sterling, and Robert Harper. MFPS 2024 Slides.
• Decalf: A Directed, Effectful Cost-Aware Logical Framework. Harrison Grodin, Robert Harper, Yue Niu, and Jonathan Sterling. POPL 2024.

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. Compositional verification of cost and behavior in Calf.
• Runming Li. Cost-aware compiler correctness, verification of semantics of Calf.
• Andrew Zhou. Summer 2025 project: Cost verification of parallel scan.
• Lukas Kebuladze. Summer 2025 project: Cost verification of splay trees. Mechanization and Writeup.

Collaborators

• Stephanie Balzer. Session types for concurrency.
• Karl Crary. Certifying compilers, logical frameworks, mechanized metatheory.
• Jan Hoffmann. Cost-aware programming languages, mechanized cost analysis.
• 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

• 15-413: Advanced Topics in Principles of Programming Languages (Spring 2025).
• 15-312/15-652: Principles of Programming Languages (Fall 2025).

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 A210038S002, and AFOSR grant FA9550-23-1-0434, Tristan Nguyen, program manager.
• AFOSR under award number FA9550-21-1-0385, Tristan Nguyen, program manager.
• Jane Street Group, LLC.

Last modified: