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$ Jan 12 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
    Jan 12 at 20:28
  • 1
    $\begingroup$ You might also like this paper: dl.acm.org/doi/10.1145/3158111 $\endgroup$ Jan 21 at 23:10


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.