Abstraction Functions as Types
Harrison Grodin, Runming Li, and Robert
Harper
Preprint 2025 (paper)
I'm a graduate student at the Computer Science Department of Carnegie Mellon University. I'm a member of the PoP group at CMU, and I'm advised by Robert Harper. I study programming languages from the lens of type theory and category theory.
Lately my research focuses on a dependent type theory specialized for cost analysis called the cost aware logical framework (calf).
Previously, I obtained my bachelor's degree at CMU in 2023, majoring in Computer Science, with a concentration in Principles of Programming Languages.
Here are some links: LinkedIn, GitHub, Google Scholar.
Abstraction Functions as Types
Harrison Grodin, Runming Li, and Robert
Harper
Preprint 2025 (paper)
A Verified Cost Analysis of Joinable Red-Black Trees
Runming Li, Harrison Grodin, and Robert
Harper
Preprint 2023 (paper)
What's in a Name? Linear Temporal Logic Literally Represents Time
Lines
Runming Li*, Keerthana Gurushankar*, Marijn Heule, and
Kristin-Yvonne Rozier
VISSOFT 2023
(paper, slide, artifact)
How to (Re)Invent Synthetic Tait Computability
CMU PLunch 2025
Higher Inductive Types
Hype for Types guest lecture 2024