Showing cs.PLShow 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.PL2025★ 2 cited
Abstraction Functions as Types
Harrison Grodin, Runming Li, Robert Harper
Software development depends on the use of libraries whose public specifications inform client code and impose obligations on private implementations; it follows that verification…