Canonicity for Cost-Aware Logical Framework via Synthetic Tait Computability
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910913012957184 |
|---|---|
| author | Li, Runming Harper, Robert |
| author_facet | Li, Runming Harper, Robert |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_12464 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Canonicity for Cost-Aware Logical Framework via Synthetic Tait Computability Li, Runming Harper, Robert Programming Languages Logic in Computer Science 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. |
| title | Canonicity for Cost-Aware Logical Framework via Synthetic Tait Computability |
| topic | Programming Languages Logic in Computer Science |
| url | https://arxiv.org/abs/2504.12464 |