Gradualizing the Calculus of Inductive Constructions
summary
Proposes a no‑go theorem: you cannot keep graduality, normalization and conservativity (closure of universes under dependent product) all at once—the Fire Triangle of Graduality. Gives three GCIC variants that each relax one corner by tweaking universe treatment, and formalizes a bidirectional elaboration GCIC → CastCIC that inserts runtime casts and errors so typing and evaluation interact safely. Proves progress/preservation, normalization where applicable, the static gradual guarantee and semantic graduality via models; prototype not yet implemented.
AI-written summary · about