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: https://www.ps.uni-saarland.de/autosubst/doc/Ssr.SystemF_SN.html (see https://www.ps.uni-saarland.de/autosubst/ for context — it's an exercise done with a new library for formalization). — Blaisorblade, Jun 14 '18 at 08:59

score 8 · Accepted Answer · answered Jun 08 '18 at 11:01

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 08 '18 at 11:01

Neel Krishnaswami

Is there an existing Coq formalization? – Łukasz Lew Jun 08 '18 at 16:37
1

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

Found two more:
Strong normalization for System F by HOAS on top of FOAS and Girard Normalization Proof in LEGO, page 67
– Łukasz Lew Jun 09 '18 at 00:49
1

Here's one in Coq! https://github.com/coq-community/autosubst/blob/master/examples/ssr/SystemF_CBV.v – cody Jun 09 '22 at 18:46

1 Answers1