School of Computer Science
Carnegie Mellon University
Email: runmingl [at] cs [dot] cmu [dot] edu
I’m a graduate student in the Computer Science Department at Carnegie Mellon University. I’m a member of the PoP group at CMU, advised by Robert Harper. I study programming languages through the lens of type theory and category theory.
My current research focuses on a dependent type theory specialized for cost analysis called the Cost-Aware Logical Framework (calf). A complete bibliography of our group’s work on calf can be found here. My current research statement (as of December 2025) can be found here.
Previously I obtained my bachelor’s degree in computer science at CMU in 2023, majoring in Computer Science, with a concentration in Principles of Programming Languages.
Links:
LinkedIn | GitHub | Google
Scholar | Semantic
Scholar | CV
Note: ACM digital library generates AI summaries for some of my papers. Such summaries are not written by nor endorsed by me or my co-authors.
Mechanizing Synthetic Tait
Computability in Istari
Runming Li, Yue Yao, and Robert
Harper
CPP
2026 (doi, pdf,
mechanization,
slides, video)
Abstraction Functions as
Types: Modular Verification of Cost and Behavior in Dependent Type
Theory
Harrison Grodin, Runming Li, and
Robert Harper
POPL 2026 (doi, pdf, mechanization, slides,
video)
Big-Stop Semantics:
Small-Step Semantics in a Big-Step Judgment
David M Kahn, Jan Hoffmann, and Runming
Li
POPL 2026 (doi, pdf, arXiv, mechanization, code, video)
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)
Canonicity for
Cost-Aware Logical Framework via Synthetic Tait
Computability
Runming Li and Robert Harper
Preprint 2025 (arXiv)
A Verified Cost Analysis of
Joinable Red-Black Trees
Runming Li, Harrison Grodin, and
Robert Harper
Preprint 2023 (arXiv)
Cost and
Behavior in Type Theory: Modularity, Metatheory, and
Mechanization
Poster at Jane Street GRF
2026
Mechanizing
Synthetic Tait Computability in Istari
CMU PLunch 2025
Mechanizing Synthetic
Tait Computability in Istari
MURI 2025
How to (Re)Invent
Synthetic Tait Computability
CMU PLunch 2025
Higher Inductive
Types
Hype for Types guest lecture
2024
I am fortunate to mentor the following undergraduate students on their research projects.