1 citations · 1 across the 2 of their papers we have counts for
4 papers
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…
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…
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…