Theoretical Computer Science
lo.logic type-systems coq normalization agda
Updated Wed, 22 Jun 2022 05:30:06 GMT

Is there a formalization of normalization of impredicative system F?

In particular Agda seems not strong enough to prove that.

Is the predicative Calculus of Inductive Constructions universes (Coq without Prop) sufficient?

How about with the impredicative Prop?


  • Coq without Prop is not strong enough, because it's basically Martin-Lf type theory with universes.

  • Coq with Prop is strong enough, because you can encode sets of normalizing terms via predicates $S : \mathrm{Term} \to \mathrm{Prop}$, and impredicative universal quantification lets you express arbitrary intersections.

Comments (4)

Linked Articles

Local articles referenced by this article: