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…