What's in a Name? Linear Temporal Logic Literally Represents Time Lines. - Runming Li; Keerthana Gurushankar; Marijn J. H. Heule; Kristin Yvonne Rozier (VISSOFT, 2023)

A Verified Cost Analysis of Joinable Red-Black Trees. - Runming Li; Harrison Grodin; Robert Harper 001 (CoRR, 2023)

Abstraction Functions as Types. - Harrison Grodin; Runming Li; Robert Harper 001 (CoRR, 2025)

Canonicity for Cost-Aware Logical Framework via Synthetic Tait Computability. - Runming Li; Robert Harper 001 (CoRR, 2025)