Fracture-and-gluing equips every Calf computation type with an abstraction-plus-potential homomorphism so programs conserve potential and preserve abstraction; credits/debits and Giralf enable banker's-view programming and AARA-style inference.
Canonicity for Cost-Aware Logical Framework via Synthetic Tait Computability
2 Pith papers cite this work, alongside 1 external citations. Polarity classification is still indexing.
2
Pith papers citing it
1
external citations · Pith
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.
years
2026 2verdicts
ACCEPT 2representative citing papers
Contravariant families in simplicial HoTT supply proof-relevant expansion, yielding directed Boolean canonicity and a binary parametricity model over reduction-aware syntax.
citing papers explorer
-
Potential Functions as Types
Fracture-and-gluing equips every Calf computation type with an abstraction-plus-potential homomorphism so programs conserve potential and preserve abstraction; credits/debits and Giralf enable banker's-view programming and AARA-style inference.
-
Directed proof-relevant logical relations in simplicial HoTT
Contravariant families in simplicial HoTT supply proof-relevant expansion, yielding directed Boolean canonicity and a binary parametricity model over reduction-aware syntax.