5 papers · 1 filter
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…
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…
Canonicity for Cost-Aware Logical Framework via Synthetic Tait Computability
Runming Li, Robert Harper
In the original work on the cost-aware logical framework by Niu et al., a dependent variant of the call-by-push-value language for cost analysis, the authors conjectured that the c…
Amortized Analysis via Coalgebra
Harrison Grodin, Robert Harper
Amortized analysis is a cost analysis technique for data structures in which cost is studied in aggregate: rather than considering the maximum cost of a single operation, one bound…
Cost-sensitive computational adequacy of higher-order recursion in synthetic domain theory
Yue Niu, Jonathan Sterling, Robert Harper
We study a cost-aware programming language for higher-order recursion dubbed in the setting of synthetic domain theory (SDT). Our main contribution rel…