added 139 characters in body
Source Link

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. That paper claims to not be the first, so which ones are earlier?

For impredicative System F, I found this question.

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 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?

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 That paper claims to not be the first, so which ones are earlier?

For impredicative System F, I found this question.

For dependent type theory, I am aware of this paper 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?

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. That paper claims to not be the first, so which ones are earlier?

For impredicative System F, I found this question.

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 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?

Source Link

For which type systems have normalizaton proofs been formalized?

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 That paper claims to not be the first, so which ones are earlier?

For impredicative System F, I found this question.

For dependent type theory, I am aware of this paper 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?