6 papers
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…
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…
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…