A cost-aware logical framework. - Yue Niu; Jonathan Sterling; Harrison Grodin; Robert Harper 001 (Proc. ACM Program. Lang., 2022)

Amortized Analysis via Coinduction (Early Ideas). - Harrison Grodin; Robert Harper 001 (CALCO, 2023)

Amortized Analysis via Coinduction. - Harrison Grodin; Robert Harper 001 (CoRR, 2023)

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

Amortized Analysis via Coalgebra. - Harrison Grodin; Robert Harper 001 (CoRR, 2024)

Decalf: A Directed, Effectful Cost-Aware Logical Framework. - Harrison Grodin; Yue Niu; Jonathan Sterling; Robert Harper 001 (Proc. ACM Program. Lang., 2024)

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