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…
Mechanizing Synthetic Tait Computability in Istari
Runming Li, Yue Yao, Robert Harper
Categorical gluing is a powerful technique for proving meta-theorems of type theories such as canonicity and normalization. Synthetic Tait Computability (STC) provides an abstract…
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…
Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment
David M Kahn, Jan Hoffmann, Runming Li
As is evident in the programming language literature, many practitioners favor specifying dynamic program behavior using big-step over small-step semantics. Unlike small-step seman…
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…