Papers

• Abstraction Functions as Types. Harrison Grodin, Runming Li, and Robert Harper. Preprint, February 2025.
• Amortized Analysis via Coalgebra. Harrison Grodin and Robert Harper. MFPS 2024 Slides.
• 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.
• 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

• 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.
• Jon Sterling, Cambridge University. Cost-aware type theory.

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 2024).

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.

Last modified: