Email Gateway (Sep 17 2026 at 15:15): Email Gateway (Sep 17 2026 at 15:15):From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] New in the AFP: Strong Normalization for Church-Style System F
A new entry by Arthur Freitas Ramos, David Barros Hulak, and Ruy Jose Guerra Barretto de Queiroz—this time a computer science classic. The introduction explains the relationship to existing Isabelle proofs of strong normalization for weaker languages and other results for stronger languages than System F.
Strong Normalization for Church-Style System F
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.
https://isa-afp.org/entries/System_F_Normalization.html
Enjoy!
Last updated: Sep 17 2026 at 22:43 UTC