Is there a formalization of normalization of impredicative system F?

Question

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?

There's one here: ps.uni-saarland.de/autosubst/doc/Ssr.SystemF_SN.html (see ps.uni-saarland.de/autosubst for context — it's an exercise done with a new library for formalization). — Blaisorblade, Jun 14, 2018 at 8:59

Neel Krishnaswami · Accepted Answer · 2018-06-08 11:01:45Z

8

Coq without Prop is not strong enough, because it's basically Martin-Löf 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.

answered Jun 8, 2018 at 11:01

Neel Krishnaswami

32.1k1 gold badge98 silver badges164 bronze badges

$\begingroup$ Is there an existing Coq formalization? $\endgroup$
– Łukasz Lew
Jun 8, 2018 at 16:37
1

$\begingroup$ @ŁukaszLew I couldn't find anything compelling online, but there is a Lego formalization by Altenkirch (1993!) described here: cs.nott.ac.uk/~psztxa/publ/tlca93.pdf $\endgroup$
– cody
Jun 8, 2018 at 19:12
1

$\begingroup$ Found two more: Strong normalization for System F by HOAS on top of FOAS and Girard Normalization Proof in LEGO, page 67 $\endgroup$
– Łukasz Lew
Jun 9, 2018 at 0:49
$\begingroup$ Here's one in Coq! github.com/coq-community/autosubst/blob/master/examples/ssr/… $\endgroup$
– cody
Jun 9, 2022 at 18:46

Add a comment |

1 Answer 1