Abstract
This entry formalizes strong normalization for Church-style System F with explicit type abstraction and type application. Types and terms use de Bruijn indices; the reduction relation contains both term-\(\beta\) and type-\(\beta\) steps and is closed under all term contexts. The proof combines Girard-style reducibility candidates for an untyped lambda-calculus erasure with an explicit type-syntax measure that reflects the erased normalization result back to the full calculus. The final theorem states that every well-typed System F term is strongly normalizing, so the usual closed-term result is an immediate instance.
License
Note
AI assistance was used for proof engineering. The final definitions, statements, and proofs are checked by Isabelle.
Topics
- Computer science/Programming languages/Lambda calculi
- Computer science/Programming languages/Type systems
- Logic/General logic/Mechanization of proofs
Related publications
- Altenkirch, T. A formalization of the strong normalization proof for System F in LEGO. Typed Lambda Calculi and Applications, 13–28. https://doi.org/10.1007/bfb0037095
- Donnelly, K., & Xi, H. (2007). A Formalization of Strong Normalization for Simply-Typed Lambda-Calculus and System F. Electronic Notes in Theoretical Computer Science, 174(5), 109–125. https://doi.org/10.1016/j.entcs.2007.01.021
- Popescu, A., Gunter, E. L., & Osborn, C. J. (2010). Strong Normalization for System F by HOAS on Top of FOAS. 2010 25th Annual IEEE Symposium on Logic in Computer Science, 31–40. https://doi.org/10.1109/lics.2010.48
- Stefan Berghofer, POPLmark Challenge Via de Bruijn Indices, Archive of Formal Proofs (2007): https://isa-afp.org/entries/POPLmark-deBruijn.html
- Stefan Berghofer, Strong Normalization for Simply-Typed Lambda Calculus, Isabelle/HOL HOL-Proofs-Lambda library: https://isabelle.in.tum.de/library/HOL/HOL-Proofs-Lambda/document.pdf