Weak Normalization for the Simply-Typed Lambda-Calculus in Twelf

Normalization for the simply-typed λ-calculus is proven in Twelf, an implementation of the Edinburgh Logical Framework. Since due to proof-theoretical restrictions Twelf Tait’s computability method does not seem to be directly usable, a syntactical proof is adapted and formalized instead. In this case study, some boundaries of Twelf current capabilities are touched and discussed