Canonicity for Cost-Aware Logical Framework via Synthetic Tait Computability
Programming Languages
2025-04-18 v1 Logic in Computer Science
Abstract
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 canonicity property of the type theory can be succinctly proved via Sterling's synthetic Tait computability. This work resolves the conjecture affirmatively.
Cite
@article{arxiv.2504.12464,
title = {Canonicity for Cost-Aware Logical Framework via Synthetic Tait Computability},
author = {Runming Li and Robert Harper},
journal= {arXiv preprint arXiv:2504.12464},
year = {2025}
}