activity
20232026
most citedAbstraction Functions as Types

2 citations · 3 across the 7 of their papers we have counts for

collaborators
Showing 2026Show all

2 papers · 1 filter

cs.PL2026

Potential Functions as Types

Harrison Grodin, Ethan Chu, Runming Li +2

Amortized analysis can be framed from the physicist's view, amenable to manual verification in dependent type theory using potential functions, and the banker's view, amenable to a…

cs.LO2026

Directed proof-relevant logical relations in simplicial HoTT

Runming Li, Harrison Grodin, Robert Harper

Intrinsically-typed presentations of type theory often use equality in the meta-language to represent object-language judgmental equality. In such equational syntax, proof-relevant…