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?

  • 2
    $\begingroup$ Are you aware of the Coq in Coq paper? It formalizes the strong normalization proof for the calculus of constructions. $\endgroup$ Commented Jan 12, 2022 at 6:11
  • $\begingroup$ @paulotorrens So contrary to my assumptions, there is very little gap between paper proofs of normalization and formalized ones? Thanks. $\endgroup$
    – while1fork
    Commented Jan 12, 2022 at 20:28
  • 1
    $\begingroup$ You might also like this paper: dl.acm.org/doi/10.1145/3158111 $\endgroup$ Commented Jan 21, 2022 at 23:10


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.