<p>I am trying to understand what the open problems are in the area of formalizing proofs of normalization for type systems.</p>
<p>Obviously STLC has been done many times.</p>
<p>For predicative System F, I found one instance: <a href="https://sozeau.gitlabpages.inria.fr/www/research/publications/Equations_for_Hereditary_Substitution_in_Leivants_Predicative_System_F:_a_case_study.pdf" rel="noreferrer">Equations for Hereditary Substitution in Leivant’s Predicative System F: a case study</a>. That paper claims to not be the first, so which ones are earlier?</p>
<p>For impredicative System F, I found <a href="https://cstheory.stackexchange.com/questions/40942/is-there-a-formalization-of-normalization-of-impredicative-system-f">this question</a>.</p>
<p>For anything in between predicative System F and dependent type theory, I haven't found anything. Are there any results in this area?</p>
<p>For dependent type theory, I am aware of <a href="https://arxiv.org/pdf/1612.02462.pdf" rel="noreferrer">this paper</a> which uses a QIT approach by Thorsten Altenkirch and Ambrus Kaposi. I am somewhat confused by the statement that the paper makes &quot;some of the naturality and functoriality properties
are left as holes&quot;. Does this imply that <strong>formalization of normalization of dependent type theory is still an open problem?</strong></p>
<p>Also, <strong>is a formalization of normalization for dependent type theory without QITs an open problem?</strong></p>

CC BY-SA 4.0
2022-01-12T06:11:57.607Z
Are you aware of the [Coq in Coq](http://www.lix.polytechnique.fr/Labo/Bruno.Barras/publi/coqincoq.pdf) paper? It formalizes the strong normalization proof for the calculus of constructions.
paulotorrens
CC BY-SA 4.0
2022-01-12T20:28:21.403Z
@paulotorrens So contrary to my assumptions, there is very little gap between paper proofs of normalization and formalized ones? Thanks.
while1fork
CC BY-SA 4.0
2022-01-21T23:10:08.253Z
You might also like this paper: https://dl.acm.org/doi/10.1145/3158111
Joey Eremondi
<type-theory><dependent-type><embeddings>
For which type systems have normalizaton proofs been formalized?
while1fork
# For which type systems have normalizaton proofs been formalized?

(Asked by: username_0 on 2022-01-11)

I am trying to understand what the open problems are in the area of formalizing proofs of normalization for type systems.

Obviously STLC has been done many times.

For predicative System F, I found one instance: [Equations for Hereditary Substitution in Leivant’s Predicative System F: a case study](https://sozeau.gitlabpages.inria.fr/www/research/publications/Equations_for_Hereditary_Substitution_in_Leivants_Predicative_System_F:_a_case_study.pdf). That paper claims to not be the first, so which ones are earlier?

For impredicative System F, I found [this question](https://cstheory.stackexchange.com/questions/40942/is-there-a-formalization-of-normalization-of-impredicative-system-f).

For anything in between predicative System F and dependent type theory, I haven't found anything. Are there any results in this area?

For dependent type theory, I am aware of [this paper](https://arxiv.org/pdf/1612.02462.pdf) which uses a QIT approach by Thorsten Altenkirch and Ambrus Kaposi. I am somewhat confused by the statement that the paper makes "some of the naturality and functoriality properties
are left as holes". Does this imply that **formalization of normalization of dependent type theory is still an open problem?**

Also, **is a formalization of normalization for dependent type theory without QITs an open problem?**

**Tags:** type-theory, dependent-type, embeddings

> **Comments:**
> **username_1**: Are you aware of the [Coq in Coq](http://www.lix.polytechnique.fr/Labo/Bruno.Barras/publi/coqincoq.pdf) paper? It formalizes the strong normalization proof for the calculus of constructions.  
> **username_0**: @username_1 So contrary to my assumptions, there is very little gap between paper proofs of normalization and formalized ones? Thanks.  
> **username_2**: You might also like this paper: https://dl.acm.org/doi/10.1145/3158111  

---

## 0 answers

